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. --- tactics/autorewrite.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/autorewrite.ml') diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index f43f4b250..e58ec5a31 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -92,7 +92,7 @@ type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg. let one_base general_rewrite_maybe_in tac_main bas = let lrul = find_rewrites bas in let try_rewrite dir ctx c tc = - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c in -- cgit v1.2.3