4 files changed, 13 insertions, 13 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index f271c14ea..f83f262b4 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -264,19 +264,19 @@ val e_new_evar :
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool -> ?hypnaming:naming_mode -> types -> constr
-[@@ocaml.deprecated "Use [Evd.new_evar]"]
+[@@ocaml.deprecated "Use [Evarutil.new_evar]"]
 
 val e_new_type_evar : env -> evar_map ref ->
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
   ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t
-[@@ocaml.deprecated "Use [Evd.new_type_evar]"]
+[@@ocaml.deprecated "Use [Evarutil.new_type_evar]"]
 
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
-[@@ocaml.deprecated "Use [Evd.new_Type]"]
+[@@ocaml.deprecated "Use [Evarutil.new_Type]"]
 
 val e_new_global : evar_map ref -> GlobRef.t -> constr
-[@@ocaml.deprecated "Use [Evd.new_global]"]
+[@@ocaml.deprecated "Use [Evarutil.new_global]"]
 
 val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst
 [@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
diff --git a/engine/proofview.ml b/engine/proofview.ml
index fdb0a215d..b4afb6415 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -39,7 +39,7 @@ let proofview p =
 
 let compact el ({ solution } as pv) =
   let nf c = Evarutil.nf_evar solution c in
-  let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in
+  let nf0 c = EConstr.(to_constr solution (of_constr c)) in
   let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
   let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
   let pruned_solution = Evd.drop_all_defined solution in
diff --git a/engine/termops.ml b/engine/termops.ml
index 0c567754a..eacc36107 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -781,24 +781,23 @@ let map_constr_with_full_binders sigma g f l cstr =
 
 let fold_constr_with_full_binders sigma g f n acc c =
   let open RelDecl in
-  let inj c = EConstr.Unsafe.to_constr c in
   match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
-  | Lambda (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
-  | LetIn (na,b,t,c) -> f (g (LocalDef (na, inj b, inj t)) n) (f n (f n acc b) t) c
+  | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (p,c) -> f n acc c
   | Evar (_,l) -> Array.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
   | CoFix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
diff --git a/engine/termops.mli b/engine/termops.mli
index 6e63539ca..255494031 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -75,8 +75,9 @@ val fold_constr_with_binders : Evd.evar_map ->
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
 val fold_constr_with_full_binders : Evd.evar_map ->
-  (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
-    'a -> 'b -> constr -> 'b
+  (rel_declaration -> 'a -> 'a) ->
+  ('a -> 'b -> constr -> 'b) ->
+  'a -> 'b -> constr -> 'b
 
 val iter_constr_with_full_binders : Evd.evar_map ->
   (rel_declaration -> 'a -> 'a) ->