diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index c9ac9419c8..9c8f2fa101 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -270,8 +270,12 @@ val destLambda : constr -> name * types * constr val destLetIn : constr -> name * constr * types * constr (* Destructs an application *) +val destApp : constr -> constr * constr array + +(* Obsolete synonym of destApp *) val destApplication : constr -> constr * constr array -(* ... removing casts *) + +(* Decompose any term as an applicative term; the list of args can be empty *) val decompose_app : constr -> constr * constr list (* Destructs a constant *) @@ -410,6 +414,9 @@ 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 + (*s Occur checks *) (* [closed0 M] is true iff [M] is a (deBruijn) closed term *) |