diff options
Diffstat (limited to 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 55e6b6533f..6b8f131f41 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -76,3 +76,5 @@ val map_pattern : (glob_constr -> glob_constr) -> val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr + +val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list |