From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 ide/ideproof.ml | 40 ++++++++++++++++++++++++----------------
 1 file changed, 24 insertions(+), 16 deletions(-)

(limited to 'ide/ideproof.ml')

diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index b79d6469..697e7f4f 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -109,31 +109,39 @@ let mode_cesar (proof:GText.view) = function
       proof#buffer#insert ("thesis := \n "^cur_goal^"\n");
       ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
 
+let rec flatten = function
+| [] -> []
+| (lg, rg) :: l ->
+  let inner = flatten l in
+  List.rev_append lg inner @ rg
+
 let display mode (view:GText.view) goals hints evars =
   let () = view#buffer#set_text "" in
   match goals with
   | None -> ()
     (* No proof in progress *)
-  | Some { Interface.fg_goals = []; Interface.bg_goals = [] } ->
-    (* A proof has been finished, but not concluded *)
-    begin match evars with
-    | Some evs when evs <> [] ->
+  | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
+    let bg = flatten (List.rev bg) in
+    let evars = match evars with None -> [] | Some evs -> evs in
+    begin match (bg, evars) with
+    | [], [] ->
+      view#buffer#insert "No more subgoals."
+    | [], _ :: _ ->
+      (* A proof has been finished, but not concluded *)
       view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
       let iter evar =
         let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
         view#buffer#insert msg
       in
-      List.iter iter evs
-    | _ ->
-      view#buffer#insert "No more subgoals."
+      List.iter iter evars
+    | _, _ ->
+      (* 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 msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
+        view#buffer#insert msg
+      in
+      List.iter iter bg
     end
-  | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
-    (* 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 msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-      view#buffer#insert msg
-    in
-    List.iter iter bg
   | Some { Interface.fg_goals = fg } ->
     mode view fg hints
-- 
cgit v1.2.3