From 3c1cd2338fcddc4a6c0e97b0af53eb2b2f238c4a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/contradiction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/contradiction.ml')

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 0e28aa980..63f923dfd 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -110,7 +110,7 @@ let is_negation_of env sigma typ t =
     | _ -> false
 
 let contradiction_term (c,lbind as cl) =
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter { enter = begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
-- 
cgit v1.2.3