Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Print "n focused goals / x shelved / ID y" in 1 line #14999

Merged
merged 1 commit into from
Oct 11, 2021
Merged

Print "n focused goals / x shelved / ID y" in 1 line #14999

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
4 changes: 2 additions & 2 deletions printing/printer.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -771,8 +771,8 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
let goals = print_multiple_goals g1 rest in
let ngoals = List.length rest+1 in
v 0 (
int ngoals ++ focused_if_needed ++ str(String.plural ngoals "goal")
++ print_extra
hov 0 (int ngoals ++ focused_if_needed ++ str(String.plural ngoals "goal")
++ print_extra)
++ str (if pr_first && (should_gname()) && ngoals > 1 then ", goal 1" else "")
++ (if pr_first && should_tag() then pr_goal_tag g1 else str"")
++ (if pr_first then pr_goal_name sigma g1 else mt()) ++ cut () ++ goals
Expand Down
6 changes: 2 additions & 4 deletions test-suite/output-coqtop/DependentEvars.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,8 +50,7 @@ Coq < Coq < 1 goal
(dependent evars: ; in current goal:)

p14 <
p14 < 4 focused goals
(shelved: 2)
p14 < 4 focused goals (shelved: 2)

P1, P2, P3, P4 : Prop
p12 : P1 -> P2
Expand All @@ -69,8 +68,7 @@ goal 4 is:

(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)

p14 < 3 focused goals
(shelved: 2)
p14 < 3 focused goals (shelved: 2)

P1, P2, P3, P4 : Prop
p12 : P1 -> P2
Expand Down
12 changes: 4 additions & 8 deletions test-suite/output-coqtop/DependentEvars2.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,7 @@ Coq < Coq < 1 goal
p14 <
p14 < Second proof:

p14 < 4 focused goals
(shelved: 2)
p14 < 4 focused goals (shelved: 2)

P1, P2, P3, P4 : Prop
p12 : P1 -> P2
Expand All @@ -71,8 +70,7 @@ goal 4 is:

(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)

p14 < 1 focused goal
(shelved: 2)
p14 < 1 focused goal (shelved: 2)

P1, P2, P3, P4 : Prop
p12 : P1 -> P2
Expand All @@ -86,8 +84,7 @@ p14 < 1 focused goal
p14 < This subproof is complete, but there are some unfocused goals.
Try unfocusing with "}".

3 goals
(shelved: 2)
3 goals (shelved: 2)

goal 1 is:
?P -> (?P0 -> P4) /\ ?P0
Expand All @@ -98,8 +95,7 @@ goal 3 is:

(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal:)

p14 < 3 focused goals
(shelved: 2)
p14 < 3 focused goals (shelved: 2)

P1, P2, P3, P4 : Prop
p12 : P1 -> P2
Expand Down
141 changes: 68 additions & 73 deletions test-suite/output-coqtop/ShowGoal.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,73 +1,68 @@

Coq < 1 goal

============================
forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k

x <
x < 1 focused goal
(shelved: 1)

i : nat
============================
exists k : nat, i = ?j /\ ?j = k /\ i = k

x < 1 focused goal
(shelved: 2)

i : nat
============================
i = ?j /\ ?j = ?k /\ i = ?k

x < 2 focused goals
(shelved: 2)

i : nat
============================
i = ?j

goal 2 is:
?j = ?k /\ i = ?k

x < 1 focused goal
(shelved: 1)

i : nat
============================
i = ?k /\ i = ?k

x < 2 focused goals
(shelved: 1)

i : nat
============================
i = ?k

goal 2 is:
i = ?k

x < 1 goal

i : nat
============================
i = i

x < goal ID 13 at state 5

i : nat
============================
i = ?j /\ ?j = ?k /\ i = ?k

x < goal ID 13 at state 7

i : nat
============================
i = i /\ i = ?k /\ i = ?k

x < goal ID 13 at state 9

i : nat
============================
i = i /\ i = i /\ i = i

x <

Coq < 1 goal

============================
forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k

x <
x < 1 focused goal (shelved: 1)

i : nat
============================
exists k : nat, i = ?j /\ ?j = k /\ i = k

x < 1 focused goal (shelved: 2)

i : nat
============================
i = ?j /\ ?j = ?k /\ i = ?k

x < 2 focused goals (shelved: 2)

i : nat
============================
i = ?j

goal 2 is:
?j = ?k /\ i = ?k

x < 1 focused goal (shelved: 1)

i : nat
============================
i = ?k /\ i = ?k

x < 2 focused goals (shelved: 1)

i : nat
============================
i = ?k

goal 2 is:
i = ?k

x < 1 goal

i : nat
============================
i = i

x < goal ID 13 at state 5

i : nat
============================
i = ?j /\ ?j = ?k /\ i = ?k

x < goal ID 13 at state 7

i : nat
============================
i = i /\ i = ?k /\ i = ?k

x < goal ID 13 at state 9

i : nat
============================
i = i /\ i = i /\ i = i

x <
81 changes: 39 additions & 42 deletions test-suite/output-coqtop/ShowProofDiffs.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,42 +1,39 @@

Coq < Coq < 1 goal

============================
forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k

x <
x < 1 focused goal
(shelved: 1)
i : nat
============================
exists k : nat, i = ?j /\ ?j = k /\ i = k

(fun i : nat =>
ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) ?j ?Goal)

x < 1 focused goal
(shelved: 2)
i : nat
============================
i = ?j /\ ?j = ?k /\ i = ?k

(fun i : nat =>
ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) 
?j (ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) ?k ?Goal))

x < 2 focused goals
(shelved: 2)
i : nat
============================
i = ?j

goal 2 is:
?j = ?k /\ i = ?k

(fun i : nat =>
ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) 
?j
(ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) 
?k (conj ?Goal ?Goal0)))

x <

Coq < Coq < 1 goal

============================
forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k

x <
x < 1 focused goal (shelved: 1)
i : nat
============================
exists k : nat, i = ?j /\ ?j = k /\ i = k

(fun i : nat =>
ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) ?j ?Goal)

x < 1 focused goal (shelved: 2)
i : nat
============================
i = ?j /\ ?j = ?k /\ i = ?k

(fun i : nat =>
ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) 
?j (ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) ?k ?Goal))

x < 2 focused goals (shelved: 2)
i : nat
============================
i = ?j

goal 2 is:
?j = ?k /\ i = ?k

(fun i : nat =>
ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) 
?j
(ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) 
?k (conj ?Goal ?Goal0)))

x <
3 changes: 1 addition & 2 deletions test-suite/output/names.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,7 @@ In environment
y : nat
The term "a y" has type "{y0 : nat | y = y0}"
while it is expected to have type "{x : nat | x = y}".
1 focused goal
(shelved: 1)
1 focused goal (shelved: 1)

H : ?n <= 3 -> 3 <= ?n -> ?n = 3
============================
Expand Down
12 changes: 4 additions & 8 deletions test-suite/output/unifconstraints.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
3 focused goals
(shelved: 1)
3 focused goals (shelved: 1)

============================
?Goal 0
Expand All @@ -13,8 +12,7 @@ unification constraint:
True /\ True /\ True \/
veeryyyyyyyyyyyyloooooooooooooonggidentifier =
veeryyyyyyyyyyyyloooooooooooooonggidentifier
3 focused goals
(shelved: 1)
3 focused goals (shelved: 1)

n, m : nat
============================
Expand All @@ -29,8 +27,7 @@ unification constraint:
True /\ True /\ True \/
veeryyyyyyyyyyyyloooooooooooooonggidentifier =
veeryyyyyyyyyyyyloooooooooooooonggidentifier
3 focused goals
(shelved: 1)
3 focused goals (shelved: 1)

m : nat
============================
Expand All @@ -46,8 +43,7 @@ unification constraint:
True /\ True /\ True \/
veeryyyyyyyyyyyyloooooooooooooonggidentifier =
veeryyyyyyyyyyyyloooooooooooooonggidentifier
3 focused goals
(shelved: 1)
3 focused goals (shelved: 1)

m : nat
============================
Expand Down
15 changes: 5 additions & 10 deletions test-suite/output/unification.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,32 +9,27 @@ Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate
The command has indeed failed with message:
The term "id" has type "ID" while it is expected to have type
"Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope).
1 focused goal
(shelved: 1)
1 focused goal (shelved: 1)

H : forall x : nat, S (S (S x)) = x
============================
?x = 0
1 focused goal
(shelved: 1)
1 focused goal (shelved: 1)

H : forall x : nat, S (S (S x)) = x
============================
?x = 0
1 focused goal
(shelved: 1)
1 focused goal (shelved: 1)

H : forall x : nat, S (S (S x)) = x
============================
?x = 0
1 focused goal
(shelved: 1)
1 focused goal (shelved: 1)

H : forall x : nat, S x = x
============================
?y = 0
1 focused goal
(shelved: 3)
1 focused goal (shelved: 3)

T : Prop
H : forall Q R S : Prop, (Q /\ R) /\ S -> T
Expand Down