diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-19 01:07:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:56 +0100 |
| commit | db252cb87e9c63f400fd4fddd2d771df3160d592 (patch) | |
| tree | 25c1cb44c479ffa10e6db87f91b43f7e60b427bd /engine | |
| parent | 118ae18590dbc7d01cf34e0cd6133b1e34ef9090 (diff) | |
Inv API using EConstr.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 4 | ||||
| -rw-r--r-- | engine/termops.mli | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index c2d862f00..4ab9f0733 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 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 |