diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-26 10:54:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-26 10:54:43 +0000 |
| commit | deb4df6668b6b1ecb6b6bb2164dddc29b1215bf1 (patch) | |
| tree | 8ed112269c8cb673e5ff598525249bed6048c105 /parsing/printer.ml | |
| parent | d4a2d6a80b57485467d6141f1140c2aee577495f (diff) | |
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
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index e99dc2b1c..0a9e826f3 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 = |