Eliminating parts of the right-hand side compatibility layer

2 files changed, 15 insertions, 12 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index ecc6ab68e..abaa409bd 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -276,10 +276,11 @@ let last_arg sigma c = match EConstr.kind sigma c with
 (* Get the last arg of an application *)
 let decompose_app_vect sigma c =
   match EConstr.kind sigma c with
-  | App (f,cl) -> (EConstr.Unsafe.to_constr f, Array.map EConstr.Unsafe.to_constr cl)
-  | _ -> (EConstr.Unsafe.to_constr c,[||])
+  | App (f,cl) -> (f, cl)
+  | _ -> (c,[||])
 
 let adjust_app_list_size f1 l1 f2 l2 =
+  let open EConstr in
   let len1 = List.length l1 and len2 = List.length l2 in
   if Int.equal len1 len2 then (f1,l1,f2,l2)
   else if len1 < len2 then
@@ -698,13 +699,13 @@ let rec subst_meta bl c =
 
 let rec strip_outer_cast sigma c = match EConstr.kind sigma c with
   | Cast (c,_,_) -> strip_outer_cast sigma c
-  | _ -> EConstr.Unsafe.to_constr c
+  | _ -> c
 
 (* flattens application lists throwing casts in-between *)
 let collapse_appl sigma c = match EConstr.kind sigma c with
   | App (f,cl) ->
       let rec collapse_rec f cl2 =
-        match EConstr.kind sigma (EConstr.of_constr (strip_outer_cast sigma f)) with
+        match EConstr.kind sigma (strip_outer_cast sigma f) with
         | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
         | _ -> EConstr.mkApp (f,cl2)
       in
@@ -744,15 +745,17 @@ let my_prefix_application sigma eq_fun (k,c) by_c t =
    works if [c] has rels *)
 
 let subst_term_gen sigma eq_fun c t =
+  let open EConstr in
+  let open Vars in
   let rec substrec (k,c as kc) t =
     match prefix_application sigma eq_fun kc t with
       | Some x -> x
       | None ->
     if eq_fun sigma c t then EConstr.mkRel k
     else
-      EConstr.map_with_binders sigma (fun (k,c) -> (k+1, EConstr.Vars.lift 1 c)) substrec kc t
+      EConstr.map_with_binders sigma (fun (k,c) -> (k+1,lift 1 c)) substrec kc t
   in
-  EConstr.Unsafe.to_constr (substrec (1,c) t)
+  substrec (1,c) t
 
 let subst_term sigma c t = subst_term_gen sigma EConstr.eq_constr c t
 
diff --git a/engine/termops.mli b/engine/termops.mli
index 05604beda..426b5f34d 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -144,7 +144,7 @@ val pop : EConstr.t -> constr
 (** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq]
    as equality *)
 val subst_term_gen : Evd.evar_map ->
-  (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> constr
+  (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> EConstr.constr
 
 (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
    as equality *)
@@ -153,7 +153,7 @@ val replace_term_gen :
     EConstr.t -> EConstr.t -> EConstr.t -> constr
 
 (** [subst_term d c] replaces [d] by [Rel 1] in [c] *)
-val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> constr
+val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.constr
 
 (** [replace_term d e c] replaces [d] by [e] in [c] *)
 val replace_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.t -> constr
@@ -174,7 +174,7 @@ val prod_applist : Evd.evar_map -> EConstr.t -> EConstr.t list -> EConstr.t
 
 (** Remove recursively the casts around a term i.e.
    [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
-val strip_outer_cast : Evd.evar_map -> EConstr.t -> constr
+val strip_outer_cast : Evd.evar_map -> EConstr.t -> EConstr.constr
 
 exception CannotFilter
 
@@ -204,10 +204,10 @@ val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int
 val last_arg : Evd.evar_map -> EConstr.t -> EConstr.constr
 
 (** Force the decomposition of a term as an applicative one *)
-val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array
+val decompose_app_vect : Evd.evar_map -> EConstr.t -> EConstr.constr * EConstr.constr array
 
-val adjust_app_list_size : constr -> constr list -> constr -> constr list ->
-  (constr * constr list * constr * constr list)
+val adjust_app_list_size : EConstr.constr -> EConstr.constr list -> EConstr.constr -> EConstr.constr list ->
+  (EConstr.constr * EConstr.constr list * EConstr.constr * EConstr.constr list)
 val adjust_app_array_size : EConstr.constr -> EConstr.constr array -> EConstr.constr -> EConstr.constr array ->
   (EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.constr array)