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

1 files changed, 5 insertions, 4 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 *)