4 files changed, 107 insertions, 6 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index f722ddda79..edd93f2266 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -878,6 +878,11 @@ Controlling the effect of proof editing commands
    proved before starting the previous proof) and Coq will switch back to the
    proof of the previous assertion.
 
+.. flag:: Printing Goal Names
+
+   When turned on, the name of the goal is printed in interactive
+   proof mode, which can be useful in cases of cross references
+   between goals.
 
 Controlling memory usage
 ------------------------
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))
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.
-