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.
---
 engine/ftactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/ftactic.ml')

diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index e23a03c0c7..b371884ba4 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -61,7 +61,7 @@ let nf_enter f =
     (fun gl ->
       gl >>= fun gl ->
       Proofview.Goal.normalize gl >>= fun nfgl ->
-      Proofview.V82.wrap_exceptions (fun () -> f nfgl))
+      Proofview.V82.wrap_exceptions (fun () -> f nfgl)) [@warning "-3"]
 
 let enter f =
   bind goals
-- 
cgit v1.2.3