diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index c099504f6f..93952a4318 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -268,6 +268,12 @@ let last_arg c = match kind_of_term c with | App (f,cl) -> array_last cl | _ -> anomaly "last_arg" +(* Get the last arg of an application *) +let decompose_app_vect c = + match kind_of_term c with + | App (f,cl) -> (f, cl) + | _ -> (c,[||]) + (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate subterms of [c]; it carries an extra data [l] (typically a name list) which is processed by [g na] (which typically cons [na] to |