diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-17 20:12:55 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:06 +0100 |
| commit | e4d93d1cef27d3a8c1e36139fc1e118730406f67 (patch) | |
| tree | 0149d4c6ff1fc4cc978e796f303ee6dcdda65074 /intf | |
| parent | 50970e4043d73d9a4fbd17ffe765745f6d726317 (diff) | |
Adding general support for irrefutable disjunctive patterns.
This now works not only for parsing of fun/forall (as in 8.6), but
also for arbitraty notations with binders and for printing.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/glob_term.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/glob_term.ml b/intf/glob_term.ml index 61bbe2c26..3f48fa547 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -105,7 +105,7 @@ type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g type 'a extended_glob_local_binder_r = | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option - | GLocalPattern of ('a cases_pattern_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g + | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g |