Check if recursive calls are guarded before printing "Proof completed".

(G_decl_mode.pr_open_subgoals still not reactivated...)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14158 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 28 insertions, 10 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index e99dc2b1c6..0a9e826f30 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -311,7 +311,7 @@ let default_pr_subgoal n sigma =
   prrec n
 
 (* Print open subgoals. Checks for uninstantiated existential variables *)
-let default_pr_subgoals close_cmd sigma = function
+let default_pr_subgoals close_cmd check_guard sigma = function
   | [] ->
       begin
 	match close_cmd with
@@ -321,7 +321,11 @@ let default_pr_subgoals close_cmd sigma = function
 	| None ->
 	    let exl = Evarutil.non_instantiated sigma in
 	      if exl = [] then
-		(str"Proof completed." ++ fnl ())
+                if check_guard () then
+		  (str"Proof completed." ++ fnl ())
+                else
+                  (str"No more subgoals but unguarded recursive calls." ++
+                   fnl ())
 	      else
 		let pei = pr_evars_int 1 exl in
 		  (str "No more subgoals but non-instantiated existential " ++
@@ -349,7 +353,7 @@ let default_pr_subgoals close_cmd sigma = function
 
 
 type printer_pr = {
- pr_subgoals            : string option -> evar_map -> goal list -> std_ppcmds;
+ pr_subgoals            : string option -> (unit -> bool) -> evar_map -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 }
@@ -371,24 +375,31 @@ let pr_goal     x = !printer_pr.pr_goal     x
 (* End abstraction layer                                              *)
 (**********************************************************************)
 
+let is_guarded pts =
+  let { Evd.it=gl ; sigma=sigma } = Proof.V82.top_goal pts in
+  let c = List.hd (Proof.partial_proof pts) in
+  try let _ = Inductiveops.control_only_guard (Goal.V82.env sigma gl) c in true
+  with _ -> false
+
 let pr_open_subgoals () =
   let p = Proof_global.give_me_the_proof () in
   let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in
+  let check_guard () = is_guarded p in
   begin match goals with
   | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
             begin match bgoals with
-	    | [] -> pr_subgoals None sigma goals
-	    | _ -> pr_subgoals None bsigma bgoals ++ fnl () ++ fnl () ++
+	    | [] -> pr_subgoals None check_guard sigma goals
+	    | _ -> pr_subgoals None check_guard bsigma bgoals ++ fnl () ++ fnl () ++
 		      str"This subproof is complete, but there are still unfocused goals:"
 		(* spiwack: to stay compatible with the proof general and coqide,
 		    I use print the message after the goal. It would be better to have
 		    something like:
  		      str"This subproof is complete, but there are still unfocused goals:" 
-		      ++ fnl () ++ fnl () ++ pr_subgoals None bsigma bgoals
+		      ++ fnl () ++ fnl () ++ pr_subgoals None guarded bsigma bgoals
 		    instead. But it doesn't quite work.
 		*)
 	    end
-  | _ -> pr_subgoals None sigma goals
+  | _ -> pr_subgoals None check_guard sigma goals
   end
 
 let pr_nth_open_subgoal n =
diff --git a/parsing/printer.mli b/parsing/printer.mli
index cdd2f42770..3a5c3decae 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -104,7 +104,7 @@ val pr_transparent_state   : transparent_state -> std_ppcmds
 (** Proofs *)
 
 val pr_goal                : goal sigma -> std_ppcmds
-val pr_subgoals            : string option -> evar_map -> goal list -> std_ppcmds
+val pr_subgoals            : string option -> (unit -> bool) -> evar_map -> goal list -> std_ppcmds
 val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
 val pr_concl               : int -> evar_map -> goal -> std_ppcmds
 
@@ -138,7 +138,7 @@ val pr_assumptionset : env -> Term.types Environ.ContextObjectMap.t ->std_ppcmds
 
 
 type printer_pr = {
- pr_subgoals            : string option -> evar_map -> goal list -> std_ppcmds;
+ pr_subgoals            : string option -> (unit -> bool) -> evar_map -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 };;
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 8ed3ae62d3..7c437ff567 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -38,11 +38,18 @@ let pr_goal gs =
 		       thesis ++ str " " ++  pc) ++ fnl ()
 
 (* arnaud: rebrancher ça 
+
+let is_guarded pts =
+  let { Evd.it=gl ; sigma=sigma } = Proof.V82.top_goal pts in
+  let c = List.hd (Proof.partial_proof pts) in
+  try let _ = Inductiveops.control_only_guard (Goal.V82.env sigma gl) c in true
+  with _ -> false
+
 let pr_open_subgoals () =
   let p = Proof_global.give_me_the_proof () in
   let { Evd.it = goals ; sigma = sigma } = Proof.V82.subgoals p in
   let close_cmd = Decl_mode.get_end_command p in
-  pr_subgoals close_cmd sigma goals
+  pr_subgoals close_cmd (fun () -> is_guarded p) sigma goals
 *)
 
 let pr_proof_instr instr =