diff options
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 6 |
1 files changed, 3 insertions, 3 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 |