From db252cb87e9c63f400fd4fddd2d771df3160d592 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 01:07:35 +0100
Subject: Inv API using EConstr.

---
 engine/termops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index c2d862f005..4ab9f0733f 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -224,8 +224,8 @@ let mkProd_wo_LetIn decl 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
+let it_mkProd init = List.fold_left (fun c (n,t)  -> EConstr.mkProd (n, t, c)) init
+let it_mkLambda init = List.fold_left (fun c (n,t)  -> EConstr.mkLambda (n, t, c)) init
 
 let it_named_context_quantifier f ~init =
   List.fold_left (fun c d -> f d c) init
-- 
cgit v1.2.3