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

2 files changed, 13 insertions, 5 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 65bf7a565d..e62b10b791 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -375,10 +375,12 @@ let destLetIn c = match kind_of_term c with
   | _ -> invalid_arg "destProd"
 
 (* Destructs an application *)
-let destApplication c = match kind_of_term c with
+let destApp c = match kind_of_term c with
   | App (f,a) -> (f, a)
   | _ -> invalid_arg "destApplication"
 
+let destApplication = destApp
+
 let isApp c = match kind_of_term c with App _ -> true | _ -> false
 
 (* Destructs a constant *)
@@ -438,10 +440,9 @@ let rec collapse_appl c = match kind_of_term c with
       collapse_rec f cl
   | _ -> c
 
-let rec decompose_app c =
-  match kind_of_term (collapse_appl c) with
+let decompose_app c =
+  match kind_of_term c with
     | App (f,cl) -> (f, Array.to_list cl)
-    | Cast (c,t) -> decompose_app c
     | _ -> (c,[])
 
 (* strips head casts and flattens head applications *)
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 *)