Merge PR #13140: Documenting Set Printing Goal Names + a small goal display fix

Reviewed-by: ejgallego
Reviewed-by: Zimmi48

2 files changed, 99 insertions, 3 deletions

diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out
index 773533a8d3..17c1aaa55b 100644
--- a/test-suite/output/goal_output.out
+++ b/test-suite/output/goal_output.out
@@ -2,7 +2,79 @@ Nat.t = nat
      : Set
 Nat.t = nat
      : Set
+2 subgoals
+  
+  ============================
+  True
+
+subgoal 2 is:
+ True
+2 subgoals, subgoal 1 (?Goal)
+  
+  ============================
+  True
+
+subgoal 2 (?Goal0) is:
+ True
 1 subgoal
   
   ============================
-  False
+  True
+1 subgoal (?Goal0)
+  
+  ============================
+  True
+1 subgoal (?Goal0)
+  
+  ============================
+  True
+
+*** Unfocused goals:
+
+subgoal 2 (?Goal1) is:
+ True
+subgoal 3 (?Goal) is:
+ True
+1 subgoal
+  
+  ============================
+  True
+
+*** Unfocused goals:
+
+subgoal 2 is:
+ True
+subgoal 3 is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+2 subgoals
+
+subgoal 1 is:
+ True
+subgoal 2 is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+2 subgoals
+
+subgoal 1 (?Goal0) is:
+ True
+subgoal 2 (?Goal) is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+1 subgoal
+
+subgoal 1 is:
+ True
+This subproof is complete, but there are some unfocused goals.
+Focus next goal with bullet -.
+
+1 subgoal
+
+subgoal 1 (?Goal) is:
+ True
diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v
index 327b80b0aa..b1ced94054 100644
--- a/test-suite/output/goal_output.v
+++ b/test-suite/output/goal_output.v
@@ -6,8 +6,32 @@
 Print Nat.t.
 Timeout 1 Print Nat.t.
 
-Lemma toto: False.
 Set Printing All.
+Lemma toto: True/\True.
+Proof.
+split.
 Show.
+Set Printing Goal Names.
+Show.
+Unset Printing Goal Names.
+assert True.
+- idtac.
+Show.
+Set Printing Goal Names.
+Show.
+Set Printing Unfocused.
+Show.
+Unset Printing Goal Names.
+Show.
+Unset Printing Unfocused.
+  auto.
+Show.
+Set Printing Goal Names.
+Show.
+Unset Printing Goal Names.
+- auto.
+Show.
+Set Printing Goal Names.
+Show.
+Unset Printing Goal Names.
 Abort.
-