diff options
Diffstat (limited to 'proofs')
| -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 |
4 files changed, 38 insertions, 10 deletions
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 |