diff options
| -rw-r--r-- | parsing/printer.ml | 3 | ||||
| -rw-r--r-- | proofs/proof.ml | 28 | ||||
| -rw-r--r-- | proofs/proof.mli | 4 | ||||
| -rw-r--r-- | proofs/proofview.ml | 11 | ||||
| -rw-r--r-- | proofs/proofview.mli | 5 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 12 |
6 files changed, 52 insertions, 11 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 0b9ce9188..0a3926660 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -363,7 +363,8 @@ let default_pr_subgoals close_cmd sigma seeds = function let pei = pr_evars_int 1 exl in (str "No more subgoals but non-instantiated existential " ++ str "variables:" ++ fnl () ++ (hov 0 pei) - ++ emacs_print_dependent_evars sigma seeds) + ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++ + str "You can use Grab Existential Variables.") end | [g] -> let pg = default_pr_goal { it = g ; sigma = sigma } in diff --git a/proofs/proof.ml b/proofs/proof.ml index 748792744..83ed0ffe1 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -445,14 +445,22 @@ module V82 = struct let top_evars p = Proofview.V82.top_evars p.state.proofview - let instantiate_evar n com pr = - let starting_point = save_state pr in - let sp = pr.state.proofview in - try - let new_proofview = Proofview.V82.instantiate_evar n com sp in - pr.state <- { pr.state with proofview = new_proofview }; - push_undo starting_point pr - with e -> - restore_state starting_point pr; - raise e + let grab_evars p = + if not (is_done p) then + raise UnfinishedProof + else + save p; + p.state <- { p.state with proofview = Proofview.V82.grab p.state.proofview } + + + let instantiate_evar n com pr = + let starting_point = save_state pr in + let sp = pr.state.proofview in + try + let new_proofview = Proofview.V82.instantiate_evar n com sp in + pr.state <- { pr.state with proofview = new_proofview }; + push_undo starting_point pr + with e -> + restore_state starting_point pr; + raise e end diff --git a/proofs/proof.mli b/proofs/proof.mli index 7c538cf0e..15ee7cf06 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -178,6 +178,10 @@ module V82 : sig (* returns the existential variable used to start the proof *) val top_evars : proof -> Evd.evar list + (* Turns the unresolved evars into goals. + Raises [UnfinishedProof] if there are still unsolved goals. *) + val grab_evars : proof -> unit + (* Implements the Existential command *) val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit end diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 0d50d521f..4246cc9c7 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -475,6 +475,17 @@ module V82 = struct let has_unresolved_evar pv = Evd.has_undefined pv.solution + (* Main function in the implementation of Grab Existential Variables.*) + let grab pv = + let goals = + List.map begin fun (e,_) -> + Goal.build e + end (Evd.undefined_list pv.solution) + in + { pv with comb = goals } + + + (* Returns the open goals of the proofview together with the evar_map to interprete them. *) let goals { comb = comb ; solution = solution } = diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 24da9d77b..fe24b54b3 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -195,6 +195,11 @@ module V82 : sig val has_unresolved_evar : proofview -> bool + (* Main function in the implementation of Grab Existential Variables. + Resets the proofview's goals so that it contains all unresolved evars + (in chronological order of insertion). *) + val grab : proofview -> proofview + (* Returns the open goals of the proofview together with the evar_map to interprete them. *) val goals : proofview -> Goal.goal list Evd.sigma diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index da35edbed..44a3b0173 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -761,3 +761,15 @@ TACTIC EXTEND is_hyp | Var _ -> tclIDTAC | _ -> tclFAIL 0 (str "Not a variable or hypothesis") ] END + + +(* Command to grab the evars left unresolved at the end of a proof. *) +(* spiwack: I put it in extratactics because it is somewhat tied with + the semantics of the LCF-style tactics, hence with the classic tactic + mode. *) +VERNAC COMMAND EXTEND GrabEvars +[ "Grab" "Existential" "Variables" ] -> + [ let p = Proof_global.give_me_the_proof () in + Proof.V82.grab_evars p; + Flags.if_verbose (fun () -> Pp.msg (Printer.pr_open_subgoals ())) () ] +END |