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

because guard condition is checked at Qed anyway and it can be expensivise to
check it twice. Use explicitly "Guarded" if you want this information.
But the wrong proof completed is now the right no more subgoals ...

Of course, we would like an incrementally checked guard condition one
day !

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

2 files changed, 9 insertions, 20 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 0a9e826f3..e8361303d 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 check_guard sigma = function
+let default_pr_subgoals close_cmd sigma = function
   | [] ->
       begin
 	match close_cmd with
@@ -321,11 +321,7 @@ let default_pr_subgoals close_cmd check_guard sigma = function
 	| None ->
 	    let exl = Evarutil.non_instantiated sigma in
 	      if exl = [] then
-                if check_guard () then
-		  (str"Proof completed." ++ fnl ())
-                else
-                  (str"No more subgoals but unguarded recursive calls." ++
-                   fnl ())
+		(str"No more subgoals." ++ fnl ())
 	      else
 		let pei = pr_evars_int 1 exl in
 		  (str "No more subgoals but non-instantiated existential " ++
@@ -353,7 +349,7 @@ let default_pr_subgoals close_cmd check_guard sigma = function
 
 
 type printer_pr = {
- pr_subgoals            : string option -> (unit -> bool) -> evar_map -> goal list -> std_ppcmds;
+ pr_subgoals            : string option -> evar_map -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 }
@@ -375,31 +371,24 @@ 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 check_guard sigma goals
-	    | _ -> pr_subgoals None check_guard bsigma bgoals ++ fnl () ++ fnl () ++
+	    | [] -> pr_subgoals None sigma goals
+	    | _ -> pr_subgoals None 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 guarded bsigma bgoals
+		      ++ fnl () ++ fnl () ++ pr_subgoals None bsigma bgoals
 		    instead. But it doesn't quite work.
 		*)
 	    end
-  | _ -> pr_subgoals None check_guard sigma goals
+  | _ -> pr_subgoals None sigma goals
   end
 
 let pr_nth_open_subgoal n =
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 3a5c3deca..cdd2f4277 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 -> (unit -> bool) -> evar_map -> goal list -> std_ppcmds
+val pr_subgoals            : string option -> 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 -> (unit -> bool) -> evar_map -> goal list -> std_ppcmds;
+ pr_subgoals            : string option -> evar_map -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 };;