diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-19 01:59:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:57 +0100 |
| commit | 7b43de20a4acd7c9da290f038d9a16fe67eccd59 (patch) | |
| tree | 14c110655c1a056c1f08557d7ffd3b0196012b3f /engine/termops.mli | |
| parent | db252cb87e9c63f400fd4fddd2d771df3160d592 (diff) | |
Leminv API using EConstr.
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 1c14e6c89..72c0cedda 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -51,9 +51,9 @@ val it_mkLambda : EConstr.constr -> (Name.t * EConstr.types) list -> EConstr.con 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 -val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types +val it_mkNamedProd_or_LetIn : EConstr.types -> Context.Named.t -> EConstr.types val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types -val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr +val it_mkNamedLambda_or_LetIn : EConstr.constr -> Context.Named.t -> EConstr.constr (* Ad hoc version reinserting letin, assuming the body is defined in the context where the letins are expanded *) |