diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-13 20:05:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:04 +0100 |
| commit | d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 (patch) | |
| tree | 4843bf72c79905f811d6f3f5ac4cdd4d81943e65 /intf | |
| parent | 7c10b4020e061fb14e01cb3abc92bb5265aa65b9 (diff) | |
Allows recursive patterns for binders to be associative on the left.
This makes treatment of recursive binders closer to the one of
recursive terms. It is unclear whether there are interesting notations
liable to use this, but this shall make easier mixing recursive
binders and recursive terms as in next commits.
Example of (artificial) notation that this commit supports:
Notation "! x .. y # A #" :=
(.. (A,(forall x, True)) ..,(forall y, True))
(at level 200, x binder).
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/notation_term.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 028d14ccf..52fd0f368 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -25,11 +25,11 @@ type notation_constr = | NVar of Id.t | NApp of notation_constr * notation_constr list | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option - | NList of Id.t * Id.t * notation_constr * notation_constr * bool + | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool (** Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr | NProd of Name.t * notation_constr * notation_constr - | NBinderList of Id.t * Id.t * notation_constr * notation_constr + | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr | NCases of Constr.case_style * notation_constr option * (notation_constr * (Name.t * (inductive * Name.t list) option)) list * |