From 7b80c5023071a0dead641da1d14078489f6e6f4c Mon Sep 17 00:00:00 2001
From: pboutill
Date: Fri, 10 Jun 2011 18:34:49 +0000
Subject: 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
---
 plugins/decl_mode/g_decl_mode.ml4 | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 7c437ff567..8ed3ae62d3 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -38,18 +38,11 @@ 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 (fun () -> is_guarded p) sigma goals
+  pr_subgoals close_cmd sigma goals
 *)
 
 let pr_proof_instr instr = 
-- 
cgit v1.2.3