diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 16 |
1 files changed, 1 insertions, 15 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 32267f6c4c..a8d9dfbfff 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -315,7 +315,7 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *) val decompose_prod_assum : types -> Context.Rel.t * types -(** Idem with lambda's *) +(** Idem with lambda's and let's *) val decompose_lam_assum : constr -> Context.Rel.t * constr (** Idem but extract the first [n] premisses, counting let-ins. *) @@ -349,20 +349,6 @@ val strip_lam_n : int -> constr -> constr val strip_prod_assum : types -> types val strip_lam_assum : constr -> constr -(** Flattens application lists *) -val collapse_appl : constr -> constr - - -(** Remove recursively the casts around a term i.e. - [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) -val strip_outer_cast : constr -> constr - -(** Apply a function letting Casted types in place *) -val under_casts : (constr -> constr) -> constr -> constr - -(** Apply a function under components of Cast if any *) -val under_outer_cast : (constr -> constr) -> constr -> constr - (** {5 ... } *) (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. Such a term can canonically be seen as the pair of a context of types |