diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 21:03:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 21:06:14 +0200 |
| commit | ba801cd1c9866f39782279e22ceab956c4efd5c6 (patch) | |
| tree | 99cc8bc1b8ad61de84a03a8eed6110f68f9bca33 /proofs | |
| parent | 7057e7e9ab1160fc0e176182b6e71f720784715a (diff) | |
Ensuring the invariant that hypotheses and named context of the environment of
Proofview goals coincide by always using the named context and discarding the
hypotheses.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 6 | ||||
| -rw-r--r-- | proofs/goal.mli | 4 | ||||
| -rw-r--r-- | proofs/proofview.ml | 11 |
3 files changed, 10 insertions, 11 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 6cdd315f8..fe8096db1 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -244,12 +244,12 @@ let refine_open_constr c = let enter f = (); fun env rdefs gl info -> let sigma = !rdefs in - f env sigma (Evd.evar_hyps info) (Evd.evar_concl info) gl + f env sigma (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 + f env sigma (Evd.evar_concl info) gl else let info = Evarutil.nf_evar_info sigma info in let sigma = Evd.add sigma gl.content info in @@ -257,7 +257,7 @@ let nf_enter f = (); fun env rdefs gl info -> 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 + f env sigma (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 diff --git a/proofs/goal.mli b/proofs/goal.mli index f887e8c66..4d3361b0e 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -133,6 +133,6 @@ 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 enter : (Environ.env -> Evd.evar_map -> Term.constr -> goal -> 'a) -> 'a sensitive -val nf_enter : (Environ.env -> Evd.evar_map -> Environ.named_context_val -> Term.constr -> goal -> 'a) -> 'a sensitive +val nf_enter : (Environ.env -> Evd.evar_map -> Term.constr -> goal -> 'a) -> 'a sensitive diff --git a/proofs/proofview.ml b/proofs/proofview.ml index e9b194c67..8a4531c12 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -837,7 +837,6 @@ module Goal = struct type 'a t = { env : Environ.env; sigma : Evd.evar_map; - hyps : Environ.named_context_val; concl : Term.constr ; self : Goal.goal ; (* for compatibility with old-style definitions *) } @@ -846,11 +845,11 @@ module Goal = struct let env { env=env } = env let sigma { sigma=sigma } = sigma - let hyps { hyps=hyps } = Environ.named_context_of_val hyps + let hyps { env=env } = Environ.named_context env let concl { concl=concl } = concl - let enter_t = Goal.nf_enter begin fun env sigma hyps concl self -> - {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self} + let enter_t = Goal.nf_enter begin fun env sigma concl self -> + {env=env;sigma=sigma;concl=concl;self=self} end let enter f = @@ -865,8 +864,8 @@ module Goal = struct tclZERO e end - let raw_enter_t f = Goal.enter begin fun env sigma hyps concl self -> - f {env=env;sigma=sigma;hyps=hyps;concl=concl;self=self} + let raw_enter_t f = Goal.enter begin fun env sigma concl self -> + f {env=env;sigma=sigma;concl=concl;self=self} end let raw_enter f = |