Cases API using EConstr.

1 files changed, 12 insertions, 2 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index e5db3c085b..16e2c04c8b 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 }