diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-16 23:59:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-07 15:27:41 +0200 |
| commit | f7cf2bccd813994e3cd98e97fe9c1c8b5cbde3cf (patch) | |
| tree | af78db19a74445cb5a2000a7947f2e806e01e78c /pretyping/glob_ops.mli | |
| parent | 495bccc436cfe72af9955b4b9d8564a8831850b9 (diff) | |
Better support for printing constructors with let-ins.
This allows e.g. to use the record notations even when there are
defined fields.
A priori fixed also missing parameters when interpreting primitive
tokens.
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 55e6b6533..6b8f131f4 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 |