diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-02-14 09:06:32 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-03-04 18:01:24 +0100 |
commit | f7153351bc1d4af2f402671c4937a5186ba77fc3 (patch) | |
tree | 4d8c043cb2da56f73be9cec543427794569edb50 /engine | |
parent | f35069aec1847068ecb501244507cb5aa9fa9b81 (diff) |
Proofview: V82.tactic option to not normalize evars
Diffstat (limited to 'engine')
-rw-r--r-- | engine/proofview.ml | 4 | ||||
-rw-r--r-- | engine/proofview.mli | 5 |
2 files changed, 6 insertions, 3 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 766ba7b35..0924b7a02 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1202,7 +1202,7 @@ let tclCHECKINTERRUPT = module V82 = struct type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - let tactic tac = + let tactic ?(nf_evars=true) tac = (* spiwack: we ignore the dependencies between goals here, expectingly preserving the semantics of <= 8.2 tactics *) (* spiwack: convenience notations, waiting for ocaml 3.12 *) @@ -1221,7 +1221,7 @@ module V82 = struct let (initgoals_w_state, initevd) = Evd.Monad.List.map (fun g_w_s s -> let g, w = drop_state g_w_s, get_state g_w_s in - let g, s = goal_nf_evar s g in + let g, s = if nf_evars then goal_nf_evar s g else g, s in goal_with_state g w, s) ps.comb ps.solution in let (goalss,evd) = Evd.Monad.List.map tac initgoals_w_state initevd in diff --git a/engine/proofview.mli b/engine/proofview.mli index cab6e3879..d2a54e238 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -550,7 +550,10 @@ val tclLIFT : 'a NonLogical.t -> 'a tactic (*** Compatibility layer with <= 8.2 tactics ***) module V82 : sig type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - val tactic : tac -> unit tactic + + (* [nf_evars=true] applies the evar (assignment) map to the goals + * (conclusion and context) before calling the tactic *) + val tactic : ?nf_evars:bool -> tac -> unit tactic (* normalises the evars in the goals, and stores the result in solution. *) |