From 6b61b63bb8626827708024cbea1312a703a54124 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Sep 2018 20:26:03 +0200
Subject: [engine] Remove and deprecate `nf_enter` et al.

After the introduction of `EConstr`, "normalization" has become
unnecessary, we thus deprecate the `nf_*` family of functions.

Test-suite and CI pass after the fix for #8513.
---
 plugins/btauto/refl_btauto.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/btauto')

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index c2bc8c079c..b0f97c59b8 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -224,7 +224,7 @@ module Btauto = struct
     Tacticals.tclFAIL 0 msg gl
 
   let try_unification env =
-    Proofview.Goal.nf_enter begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let eq = Lazy.force eq in
       let concl = EConstr.Unsafe.to_constr concl in
@@ -240,7 +240,7 @@ module Btauto = struct
     end
 
   let tac =
-    Proofview.Goal.nf_enter begin fun gl ->
+    Proofview.Goal.enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let concl = EConstr.Unsafe.to_constr concl in
       let sigma = Tacmach.New.project gl in
-- 
cgit v1.2.3