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

(limited to 'plugins/romega')

diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index e603480656..930048400a 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1049,7 +1049,7 @@ let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list =
   Tactics.apply (Lazy.force coq_I)
 
 let total_reflexive_omega_tactic unsafe =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   Coqlib.check_required_library ["Coq";"romega";"ROmega"];
   rst_omega_eq ();
   rst_omega_var ();
-- 
cgit v1.2.3