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.
---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 635bf9bf31..b7ba163309 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2009,7 +2009,7 @@ end = struct (* {{{ *)
         1 goals in
       TaskQueue.join queue;
       let assign_tac : unit Proofview.tactic =
-        Proofview.(Goal.nf_enter begin fun g ->
+        Proofview.(Goal.enter begin fun g ->
         let gid = Goal.goal g in
         let f =
           try List.assoc gid res
@@ -2301,7 +2301,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
         | `Leaks -> Exninfo.iraise exn
         | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
            let tac =
-             Proofview.Goal.nf_enter begin fun gl ->
+             Proofview.Goal.enter begin fun gl ->
                if CList.mem_f Evar.equal
                  (Proofview.Goal.goal gl) goals_to_admit then
              Proofview.give_up else Proofview.tclUNIT ()
-- 
cgit v1.2.3