4 files changed, 21 insertions, 3 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 2913645c1c..678f7c6ce6 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -445,10 +445,22 @@ let fold sigma f acc c = match kind sigma c with
 let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
   (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr nargs c1 c2
 
+let eq_einstance sigma i1 i2 =
+  let i1 = EInstance.kind sigma (EInstance.make i1) in
+  let i2 = EInstance.kind sigma (EInstance.make i2) in
+  Univ.Instance.equal i1 i2
+
+let eq_esorts sigma s1 s2 =
+  let s1 = ESorts.kind sigma (ESorts.make s1) in
+  let s2 = ESorts.kind sigma (ESorts.make s2) in
+  Sorts.equal s1 s2
+
 let eq_constr sigma c1 c2 =
   let kind c = kind_upto sigma c in
+  let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in
+  let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in
   let rec eq_constr nargs c1 c2 =
-    compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal eq_constr nargs c1 c2
+    compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2
   in
   eq_constr 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
 
@@ -461,8 +473,10 @@ let eq_constr_nounivs sigma c1 c2 =
 
 let compare_constr sigma cmp c1 c2 =
   let kind c = kind_upto sigma c in
+  let eq_inst _ _ i1 i2 = eq_einstance sigma i1 i2 in
+  let eq_sorts s1 s2 = eq_esorts sigma s1 s2 in
   let cmp nargs c1 c2 = cmp (of_constr c1) (of_constr c2) in
-  compare_gen kind (fun _ _ -> Univ.Instance.equal) Sorts.equal cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
+  compare_gen kind eq_inst eq_sorts cmp 0 (unsafe_to_constr c1) (unsafe_to_constr c2)
 
 let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
   let open UnivProblem in
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