diff options
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 |