diff options
| -rw-r--r-- | parsing/printer.ml | 25 | ||||
| -rw-r--r-- | parsing/printer.mli | 4 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 9 |
3 files changed, 10 insertions, 28 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 0a9e826f30..e8361303d6 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 3a5c3decae..cdd2f42770 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; };; 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 = |