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
---
 printing/printer.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index a1a2d9ae51..bc26caefbe 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -765,9 +765,9 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
       v 0 (
         int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal")
         ++ print_extra
-        ++ str (if (should_gname()) then ", subgoal 1" else "")
-        ++ (if should_tag() then pr_goal_tag g1 else str"")
-        ++ pr_goal_name sigma g1 ++ cut () ++ goals
+        ++ str (if pr_first && (should_gname()) && ngoals > 1 then ", subgoal 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
         ++ (if unfocused=[] then str ""
            else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut()
                  ++ pr_rec (List.length rest + 2) unfocused))
-- 
cgit v1.2.3