diff options
| -rw-r--r-- | proofs/goal.ml | 13 | ||||
| -rw-r--r-- | proofs/goal.mli | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 16 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 1 |
4 files changed, 20 insertions, 12 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 5bbc502bd..1ada11745 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -246,6 +246,19 @@ let enter f = (); fun env rdefs gl info -> let sigma = !rdefs in f env sigma (Evd.evar_hyps info) (Evd.evar_concl info) gl +let nf_enter f = (); fun env rdefs gl info -> + let sigma = !rdefs in + if gl.cache == sigma then + f env sigma (Evd.evar_hyps info) (Evd.evar_concl info) gl + else + let info = Evarutil.nf_evar_info sigma info in + let sigma = Evd.add sigma gl.content info in + let gl = { gl with cache = sigma } in + let () = rdefs := sigma in + let hyps = Evd.evar_hyps info in + let env = Environ.reset_with_named_context hyps env in + f env sigma hyps (Evd.evar_concl info) gl + (* Layer to implement v8.2 tactic engine ontop of the new architecture. Types are different from what they used to be due to a change of the internal types. *) diff --git a/proofs/goal.mli b/proofs/goal.mli index 535a2f2b1..f887e8c66 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -134,3 +134,5 @@ val refine_open_constr : Evd.open_constr -> subgoals sensitive (* [enter] combines [env], [defs], [hyps] and [concl] in a single primitive. *) val enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive + +val nf_enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 388c60c3f..32df96097 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -849,25 +849,19 @@ module Goal = struct let hyps { hyps=hyps } = Environ.named_context_of_val hyps let concl { concl=concl } = concl - let enter_t f = Goal.enter begin fun env sigma hyps concl self -> - let concl = Reductionops.nf_evar sigma concl in - let map_nf c = Reductionops.nf_evar sigma c in - let hyps = Environ.map_named_val map_nf hyps in - let env = Environ.reset_with_named_context hyps env in - f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self} + let enter_t = Goal.nf_enter begin fun env sigma hyps concl self -> + {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self} end let enter f = (* the global environment of the tactic is changed to that of the goal *) - let f gl = Proof.set_local (env gl) (f gl) in list_iter_goal () begin fun goal () -> Proof.current >>= fun env -> tclEVARMAP >>= fun sigma -> try - (* enter_t cannot modify the sigma. *) - let (t,_) = Goal.eval (enter_t f) env sigma goal in - t + let (gl, sigma) = Goal.eval enter_t env sigma goal in + tclTHEN (V82.tclEVARS sigma) ((Proof.set_local gl.env) (f gl)) with e when catchable_exception e -> let e = Errors.push e in tclZERO e @@ -902,7 +896,7 @@ module Goal = struct | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> (** The sigma is unchanged. *) - let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in + let (gl, _) = Goal.eval enter_t env sigma goal in Some gl in tclUNIT (List.map_filter map step.comb) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 2c6e7e736..b67aee7f7 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -33,7 +33,6 @@ open Locus open Locusops open Decl_kinds open Elimschemes -open Goal open Environ open Tacinterp open Termops |