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.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'engine/termops.mli') diff --git a/engine/termops.mli b/engine/termops.mli index 013efcbcb..1c14e6c89 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -46,8 +46,8 @@ val rel_list : int -> int -> EConstr.constr list (** iterators/destructors on terms *) val mkProd_or_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 : EConstr.types -> (Name.t * EConstr.types) list -> EConstr.types +val it_mkLambda : EConstr.constr -> (Name.t * EConstr.types) list -> EConstr.constr val it_mkProd_or_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 -- cgit v1.2.3