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/ssr/ssrparser.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr/ssrparser.ml4')

diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 8b9c94f2db..a7aae5bd31 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1949,7 +1949,7 @@ ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY pr_ssraarg
 END
 
 let vmexacttac pf =
-  Goal.nf_enter begin fun gl ->
+  Goal.enter begin fun gl ->
   exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl))
   end
 
-- 
cgit v1.2.3