Unification API using EConstr.

2 files changed, 17 insertions, 16 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 16e2c04c8..c1198e05a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -164,9 +164,19 @@ let rel_list n m =
   in
   reln [] 1
 
+let local_assum (na, t) =
+  let open RelDecl in
+  let inj = EConstr.Unsafe.to_constr in
+  LocalAssum (na, inj t)
+
+let local_def (na, b, t) =
+  let open RelDecl in
+  let inj = EConstr.Unsafe.to_constr in
+  LocalDef (na, inj b, inj t)
+
 let push_rel_assum (x,t) env =
   let open RelDecl in
-  push_rel (LocalAssum (x,t)) env
+  push_rel (local_assum (x,t)) env
 
 let push_rels_assum assums =
   let open RelDecl in
@@ -278,14 +288,15 @@ let adjust_app_list_size f1 l1 f2 l2 =
     (applist (f1,extras), restl1, f2, l2)
 
 let adjust_app_array_size f1 l1 f2 l2 =
+  let open EConstr in
   let len1 = Array.length l1 and len2 = Array.length l2 in
   if Int.equal len1 len2 then (f1,l1,f2,l2)
   else if len1 < len2 then
     let extras,restl2 = Array.chop (len2-len1) l2 in
-    (f1, l1, appvect (f2,extras), restl2)
+    (f1, l1, mkApp (f2,extras), restl2)
   else
     let extras,restl1 = Array.chop (len1-len2) l1 in
-    (appvect (f1,extras), restl1, f2, l2)
+    (mkApp (f1,extras), restl1, f2, l2)
 
 (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
    subterms of [c]; it carries an extra data [l] (typically a name
@@ -321,16 +332,6 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
    time being almost those of the ML representation (except for
    (co-)fixpoint) *)
 
-let local_assum (na, t) =
-  let open RelDecl in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let open RelDecl in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 let fold_rec_types g (lna,typarray,_) e =
   let open EConstr in
   let ctxt = Array.map2_i (fun i na t -> local_assum (na, Vars.lift i t)) lna typarray in
diff --git a/engine/termops.mli b/engine/termops.mli
index 2b66c88a7..df3fdd124 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -29,7 +29,7 @@ val print_rel_context : env -> std_ppcmds
 val print_env : env -> std_ppcmds
 
 (** about contexts *)
-val push_rel_assum : Name.t * types -> env -> env
+val push_rel_assum : Name.t * EConstr.types -> env -> env
 val push_rels_assum : (Name.t * types) list -> env -> env
 val push_named_rec_types : Name.t array * types array * 'a -> env -> env
 
@@ -208,8 +208,8 @@ val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array
 
 val adjust_app_list_size : constr -> constr list -> constr -> constr list ->
   (constr * constr list * constr * constr list)
-val adjust_app_array_size : constr -> constr array -> constr -> constr array ->
-  (constr * constr array * constr * constr array)
+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)
 
 (** name contexts *)
 type names_context = Name.t list