diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:41:16 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:41:16 +0000 |
| commit | 9f24c209b2c2832f552838f365cfef5df2764715 (patch) | |
| tree | a1371bfe04c8c38c324a8da318e7aabb1247e927 /proofs | |
| parent | 8c1e25acc561767980acdccc987087f51e0e2a12 (diff) | |
Fix destruct: nf_evar prior to tactic interpretation.
Noticed in CoRN
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17028 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 18 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 |
2 files changed, 19 insertions, 3 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index dd05184c4..4bc697a60 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -643,8 +643,8 @@ module V82 = struct type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma let tactic tac = - (* spiwack: we ignore the dependencies between goals here, expectingly - preserving the semantics of <= 8.2 tactics *) + (* spiwack: we ignore the dependencies between goals here, + expectingly preserving the semantics of <= 8.2 tactics *) (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in Proof.get >>= fun ps -> @@ -656,7 +656,7 @@ module V82 = struct let g = glsigma.Evd.it in ( g, sigma ) in - (* Old style tactics expect the goals normalized with respect to evars. *) + (* Old style tactics expect the goals normalized with respect to evars. *) let (initgoals,initevd) = Goal.list_map Goal.V82.nf_evar ps.comb ps.solution in @@ -666,6 +666,18 @@ module V82 = struct with e when catchable_exception e -> tclZERO e + + (* normalises the evars in the goals, and stores the result in + solution. *) + let nf_evar_goals = + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Proof.bind in + Proof.get >>= fun ps -> + let (goals,evd) = + Goal.list_map Goal.V82.nf_evar ps.comb ps.solution + in + Proof.set { ps with solution=evd ; comb=goals } + (* A [Proofview.tactic] version of [Refiner.tclEVARS] *) let tclEVARS evd = (* spiwack: convenience notations, waiting for ocaml 3.12 *) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 635f2fd47..adb6ec37d 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -275,6 +275,10 @@ module V82 : sig type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma val tactic : tac -> unit tactic + (* normalises the evars in the goals, and stores the result in + solution. *) + val nf_evar_goals : unit tactic + val tclEVARS : Evd.evar_map -> unit tactic val has_unresolved_evar : proofview -> bool |