diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-08 10:57:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:23 +0100 |
| commit | 67dc22d8389234d0c9b329944ff579e7056b7250 (patch) | |
| tree | 4b0d94384103f34e8b6071a214efb84904a56277 /engine/termops.mli | |
| parent | e4f066238799a4598817dfeab8a044760ab670de (diff) | |
Cases API using EConstr.
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index c90fdf9c2..2b66c88a7 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -45,11 +45,11 @@ val rel_list : int -> int -> constr list (** iterators/destructors on terms *) val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types -val mkProd_wo_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_or_LetIn : types -> Context.Rel.t -> types -val it_mkProd_wo_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_wo_LetIn : types -> Context.Named.t -> types @@ -170,6 +170,8 @@ val eta_reduce_head : constr -> constr (** Flattens application lists *) val collapse_appl : Evd.evar_map -> EConstr.t -> constr +val prod_applist : Evd.evar_map -> EConstr.t -> EConstr.t list -> EConstr.t + (** Remove recursively the casts around a term i.e. [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) val strip_outer_cast : Evd.evar_map -> EConstr.t -> constr |