From 3c2723f77f5ab070f8232ce0cc626875120cfe41 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Oct 2014 19:34:49 +0200
Subject: In convert_concl/convert_hyp: nf_enter -> enter. (Maybe one of the
 source of inefficiency introduced on Oct 9 - see e.g. CoLoR.)

---
 tactics/tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d131e2d33d..26b05c68ec 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -120,7 +120,7 @@ let introduction    = Tacmach.introduction
 let refine          = Tacmach.refine
 
 let convert_concl ?(check=true) ty k =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let conclty = Proofview.Goal.raw_concl gl in
@@ -139,7 +139,7 @@ let convert_concl ?(check=true) ty k =
   end
 
 let convert_hyp ?(check=true) d =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let ty = Proofview.Goal.raw_concl gl in
-- 
cgit v1.2.3