From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Dec 2016 10:45:19 +0100 Subject: Removing most nf_enter in tactics. Now they are useless because all of the primitives are (should?) be evar-insensitive. --- proofs/clenvtac.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs/clenvtac.ml') diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 32c887ff5..0722ea047 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -105,8 +105,8 @@ let dft = default_unify_flags let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = Proofview.Goal.enter { enter = begin fun gl -> - let clenv gl = clenv_unique_resolver ~flags clenv gl in - clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl)) + let clenv = clenv_unique_resolver ~flags clenv gl in + clenv_refine with_evars ~with_classes clenv end } (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en -- cgit v1.2.3