[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.

20 files changed, 37 insertions, 33 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 1eea2443fe..4f3d793ed4 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -219,7 +219,7 @@ General deprecation
 
 Proof engine
 
-  Due to the introduction of `EConstr` in 8.7, it is not necessary to
+- Due to the introduction of `EConstr` in 8.7, it is not necessary to
   track "goal evar normal form status" anymore, thus the type `'a
   Proofview.Goal.t` loses its ghost argument. This may introduce some
   minor incompatibilities at the typing level. Code-wise, things
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
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 6c389b2d67..3c4fa6f4e8 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -42,6 +42,8 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
 (** {5 Focussing} *)
 
 val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t
+[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]
+
 (** Enter a goal. The resulting tactic is focussed. *)
 
 val enter : (Proofview.Goal.t -> 'a t) -> 'a t
diff --git a/engine/proofview.mli b/engine/proofview.mli
index a9666e4f90..0bb3229a9b 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -497,6 +497,7 @@ module Goal : sig
 
   (** Normalises the argument goal. *)
   val normalize : t -> t tactic
+  [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"]
 
   (** [concl], [hyps], [env] and [sigma] given a goal [gl] return
       respectively the conclusion of [gl], the hypotheses of [gl], the
@@ -514,6 +515,7 @@ module Goal : sig
       the current goal is also given as an argument to [t]. The goal
       is normalised with respect to evars. *)
   val nf_enter : (t -> unit tactic) -> unit tactic
+  [@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]
 
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
   val enter : (t -> unit tactic) -> unit tactic
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
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index b13580bc03..3ae777cc9a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -34,7 +34,7 @@ type lseqtac= GlobRef.t -> seqtac
 type 'a with_backtracking = tactic -> 'a
 
 let wrap n b continue seq =
-  Proofview.Goal.nf_enter begin fun gls ->
+  Proofview.Goal.enter begin fun gls ->
   Control.check_for_interrupt ();
   let nc = Proofview.Goal.hyps gls in
   let env=pf_env gls in
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 73490a2dfd..b0277e9cc2 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -99,7 +99,7 @@ let let_evar name typ =
   
 let hget_evar n =
   let open EConstr in
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
   let evl = evar_list sigma concl in
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d42876e23e..ba3fa6fa0d 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -781,9 +781,9 @@ END
 (**********************************************************************)
 
 TACTIC EXTEND transparent_abstract
-| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter begin fun gl ->
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.enter begin fun gl ->
       Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ]
-| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter begin fun gl ->
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.enter begin fun gl ->
       Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ]
 END
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 414173ca79..67ffae59cc 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1469,7 +1469,7 @@ and interp_genarg ist x : Val.t Ftactic.t =
     independently of goals. *)
 
 and interp_genarg_constr_list ist x =
-  Ftactic.nf_enter begin fun gl ->
+  Ftactic.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in
@@ -1601,7 +1601,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacMutualFix (id,n,l) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin
-      Proofview.Goal.nf_enter begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = pf_env gl in
         let f sigma (id,n,c) =
           let (sigma,c_interp) = interp_type ist env sigma c in
@@ -1616,7 +1616,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacMutualCofix (id,l) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin
-      Proofview.Goal.nf_enter begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = pf_env gl in
         let f sigma (id,c) =
 	  let (sigma,c_interp) = interp_type ist env sigma c in
@@ -1696,7 +1696,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
   | TacInductionDestruct (isrec,ev,(l,el)) ->
       (* spiwack: some unknown part of destruct needs the goal to be
          prenormalised. *)
-      Proofview.Goal.nf_enter begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let sigma,l =
@@ -1723,7 +1723,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
 
   (* Conversion *)
   | TacReduce (r,cl) ->
-      Proofview.Goal.nf_enter begin fun gl ->
+      Proofview.Goal.enter begin fun gl ->
         let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in
         Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
         (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 105b5c59ae..48d677a864 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -58,7 +58,7 @@ let db_pr_goal gl =
                    str" "  ++ pc) ++ fnl ()
 
 let db_pr_goal =
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let pg = db_pr_goal gl in
   Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
   end
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index f22147f8b0..e0a369ca5f 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1456,7 +1456,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
  let ff  = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
  let vm = dump_varmap (spec.typ) (vm_of_list env) in
  (* todo : directly generate the proof term - or generalize before conversion? *)
-  Proofview.Goal.nf_enter begin fun gl -> 
+  Proofview.Goal.enter begin fun gl ->
    Tacticals.New.tclTHENLIST
     [
      Tactics.change_concl
@@ -1709,7 +1709,7 @@ let micromega_gen
     (normalise:'cst atom -> 'cst mc_cnf)
     unsat deduce 
     spec dumpexpr prover tac =
- Proofview.Goal.nf_enter begin fun gl -> 
+ Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let concl = Tacmach.New.pf_concl gl in
     let hyps  = Tacmach.New.pf_hyps_types gl in
@@ -1787,7 +1787,7 @@ let micromega_order_changer cert env ff  =
   let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
   let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
   let vm = dump_varmap (typ) (vm_of_list env) in
-  Proofview.Goal.nf_enter begin fun gl -> 
+  Proofview.Goal.enter begin fun gl ->
     Tacticals.New.tclTHENLIST
      [
      (Tactics.change_concl
@@ -1817,7 +1817,7 @@ let micromega_genr prover tac =
     proof_typ = Lazy.force coq_QWitness ;
     dump_proof = dump_psatz coq_Q dump_q
   } in
-  Proofview.Goal.nf_enter begin fun gl -> 
+  Proofview.Goal.enter begin fun gl ->
      let sigma = Tacmach.New.project gl in
      let concl = Tacmach.New.pf_concl gl in
      let hyps  = Tacmach.New.pf_hyps_types gl in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index e14c4e2ec1..abae6940fa 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -588,7 +588,7 @@ let abstract_path sigma typ path t =
 
 let focused_simpl path =
   let open Tacmach.New in
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
   convert_concl_no_check newc DEFAULTcast
   end
@@ -656,7 +656,7 @@ let new_hole env sigma c =
 
 let clever_rewrite_base_poly typ p result theorem =
   let open Tacmach.New in
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let full = pf_concl gl in
   let env = pf_env gl in
   let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
@@ -708,7 +708,7 @@ let refine_app gl t =
 
 let clever_rewrite p vpath t =
   let open Tacmach.New in
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let full = pf_concl gl in
   let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in
   let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in
@@ -1763,7 +1763,7 @@ let onClearedName id tac =
   (* so renaming may be necessary *)
   tclTHEN
     (tclTRY (clear [id]))
-    (Proofview.Goal.nf_enter begin fun gl ->
+    (Proofview.Goal.enter begin fun gl ->
      let id = fresh_id Id.Set.empty id gl in
      tclTHEN (introduction id) (tac id)
     end)
@@ -1771,7 +1771,7 @@ let onClearedName id tac =
 let onClearedName2 id tac =
   tclTHEN
     (tclTRY (clear [id]))
-    (Proofview.Goal.nf_enter begin fun gl ->
+    (Proofview.Goal.enter begin fun gl ->
      let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in
      let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in
       tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
@@ -1956,7 +1956,7 @@ let destructure_goal =
 	    try
 	      let dec = decidability t in
 	      tclTHEN
-                (Proofview.Goal.nf_enter begin fun gl ->
+                (Proofview.Goal.enter begin fun gl ->
 		                         refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |]))
 		                         end)
 	        intro
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 ();
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1f3c758e5c..f2f236f448 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1088,7 +1088,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;;
 
 (** Basic tactics *)
 
-let rec fst_prod red tac = Proofview.Goal.nf_enter begin fun gl ->
+let rec fst_prod red tac = Proofview.Goal.enter begin fun gl ->
   let concl = Proofview.Goal.concl gl in
   match EConstr.kind (Proofview.Goal.sigma gl) concl with
   | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id
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
 
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 ()
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c8fd0b7a75..8e296de617 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -162,7 +162,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
 	   | None ->
 		 (* try to rewrite in all hypothesis
 		    (except maybe the rewritten one) *)
-               Proofview.Goal.nf_enter begin fun gl ->
+               Proofview.Goal.enter begin fun gl ->
                  let ids = Tacmach.New.pf_ids_of_hyps gl in
 		 try_do_hyps (fun id -> id)  ids
                end)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9c5fdcd1ce..3456d13bbe 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -416,7 +416,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
            if get_typeclasses_filtered_unification () then
              let tac =
                matches_pattern concl p <*>
-                 Proofview.Goal.nf_enter
+                 Proofview.Goal.enter
                    (fun gl -> unify_resolve_refine poly flags gl (c,None,clenv)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0e39215701..d0f4b2c680 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -249,7 +249,7 @@ let rewrite_elim with_evars frzevars cls c e =
 
 let tclNOTSAMEGOAL tac =
   let goal gl = Proofview.Goal.goal gl in
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     let sigma = project gl in
     let ev = goal gl in
     tac >>= fun () ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 95d545b046..6999b17d8e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2824,7 +2824,7 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
 let generalize_dep ?(with_let=false) c =
   let open Tacmach.New in
   let open Tacticals.New in
-  Proofview.Goal.nf_enter begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
   let env = pf_env gl in
   let sign = Proofview.Goal.hyps gl in
   let sigma = project gl in