diff options
| author | aspiwack | 2012-02-07 16:51:46 +0000 |
|---|---|---|
| committer | aspiwack | 2012-02-07 16:51:46 +0000 |
| commit | 8e30bdf78eb5feb274b16fb1db1c7350e771ee99 (patch) | |
| tree | f79ed83ea54bce692ec865b180fc410558173410 /proofs/proof.ml | |
| parent | 5e8634d9ad5f87404e59f59888b318ca8367afc1 (diff) | |
A "Grab Existential Variables" to transform the unresolved evars at the end of a proof into goals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14973 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof.ml')
| -rw-r--r-- | proofs/proof.ml | 28 |
1 files changed, 18 insertions, 10 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 7487927445..83ed0ffe14 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 |