From 6acd4e8f15d11d4ed735092428398a3a27590f03 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 4 Oct 2020 21:51:35 +0200
Subject: Fixing redundant outputs when printing goals, especially in
 non-"pr_first" mode.

Here is an example (see test output/goal_output.v for other examples):

2 subgoals, subgoal 1 (?Goal)

subgoal 1 (?Goal) is:
 True
subgoal 2 (?Goal0) is:
 True

This is now:

2 subgoals

subgoal 1 (?Goal) is:
 True
subgoal 2 (?Goal0) is:
 True
---
 test-suite/output/goal_output.out | 74 ++++++++++++++++++++++++++++++++++++++-
 test-suite/output/goal_output.v   | 28 +++++++++++++--
 2 files changed, 99 insertions(+), 3 deletions(-)

(limited to 'test-suite')

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.
-
-- 
cgit v1.2.3