Cases API using EConstr.

2 files changed, 16 insertions, 4 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index e5db3c085..16e2c04c8 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -207,10 +207,11 @@ let mkProd_or_LetIn decl c =
 
 (* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *)
 let mkProd_wo_LetIn decl c =
+  let open EConstr in
   let open RelDecl in
   match decl with
-    | LocalAssum (na,t) -> mkProd (na, t, c)
-    | LocalDef (_,b,_) -> subst1 b c
+    | LocalAssum (na,t) -> mkProd (na, EConstr.of_constr t, c)
+    | LocalDef (_,b,_) -> Vars.subst1 (EConstr.of_constr b) c
 
 let it_mkProd init = List.fold_left (fun c (n,t)  -> mkProd (n, t, c)) init
 let it_mkLambda init = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) init
@@ -1099,6 +1100,15 @@ let global_app_of_constr sigma c =
   | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c
   | _ -> raise Not_found
 
+let prod_applist sigma c l =
+  let open EConstr in
+  let rec app subst c l =
+    match EConstr.kind sigma c, l with
+    | Prod(_,_,c), arg::l -> app (arg::subst) c l
+    | _, [] -> Vars.substl subst c
+    | _ -> anomaly (Pp.str "Not enough prod's") in
+  app [] c l
+
 (* Combinators on judgments *)
 
 let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
diff --git a/engine/termops.mli b/engine/termops.mli
index c90fdf9c2..2b66c88a7 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -45,11 +45,11 @@ val rel_list : int -> int -> constr list
 
 (** iterators/destructors on terms *)
 val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
-val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkProd_wo_LetIn : Context.Rel.Declaration.t -> EConstr.types -> EConstr.types
 val it_mkProd : types -> (Name.t * types) list -> types
 val it_mkLambda : constr -> (Name.t * types) list -> constr
 val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
-val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types
+val it_mkProd_wo_LetIn : EConstr.types -> Context.Rel.t -> EConstr.types
 val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
 val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types
 val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types
@@ -170,6 +170,8 @@ val eta_reduce_head : constr -> constr
 (** Flattens application lists *)
 val collapse_appl : Evd.evar_map -> EConstr.t -> constr
 
+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