diff options
| author | herbelin | 2005-02-12 11:29:30 +0000 |
|---|---|---|
| committer | herbelin | 2005-02-12 11:29:30 +0000 |
| commit | a1cae7a68093d0e97d1ab16f4e8d6740991a2640 (patch) | |
| tree | 7533744d7cc1d7b6b2811baad84475f11655da7c /kernel/term.mli | |
| parent | bd1e31d0e3f20e82778306bd27e0b0f8cd475757 (diff) | |
Uniformisation de destApplication en destApp; simplification decompose_app
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6712 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *) |