diff options
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 9 |
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 *) |