Granting wish #4221.

1 files changed, 12 insertions, 3 deletions

diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index b12d29d6c..a5faa60a8 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -162,12 +162,21 @@ let display mode (view : #GText.view_skel) goals hints evars =
       List.iter iter shelved_goals
     | _, _, _, _ ->
       (* No foreground proofs, but still unfocused ones *)
-      view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
-      let iter goal =
+      let total = List.length bg in
+      let goal_str index = Printf.sprintf
+        "______________________________________(%d/%d)\n" index total
+      in
+      let vb, pl = if total = 1 then "is", "" else "are", "s" in
+      let msg = Printf.sprintf "This subproof is complete, but there %s still %d \
+        unfocused goal%s:\n\n" vb total pl
+      in
+      let () = view#buffer#insert msg in
+      let iter i goal =
+        let () = view#buffer#insert (goal_str (succ i)) in
         let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
         view#buffer#insert msg
       in
-      List.iter iter bg
+      List.iteri iter bg
     end
   | Some { Interface.fg_goals = fg } ->
     mode view fg hints