diff options
| author | pboutill | 2011-06-10 18:34:49 +0000 |
|---|---|---|
| committer | pboutill | 2011-06-10 18:34:49 +0000 |
| commit | 7b80c5023071a0dead641da1d14078489f6e6f4c (patch) | |
| tree | b51d714d85937ba2281244dea1d913bcef055b3c /plugins | |
| parent | 2856df4134047a06df13f5cff3d8c62158c03779 (diff) | |
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
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 9 |
1 files changed, 1 insertions, 8 deletions
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 = |