diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-26 19:18:38 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-27 11:27:34 +0100 |
| commit | 134b220b77d74b0ada801d215a2e5c66bc6726ea (patch) | |
| tree | 27889d694009730a3fd0db51587b95c725fa26c4 /test-suite/success/Notations.v | |
| parent | c1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff) | |
Fixing associativity registered for level 10.
Apparently a long-standing bug, coupled with a pattern/constr
associativity inconsistency introduced while fixing another
pattern/constr level inconsistency (bug #4272, 0917ce7c).
Diffstat (limited to 'test-suite/success/Notations.v')
| -rw-r--r-- | test-suite/success/Notations.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index e3f90f6d9..3c0ad2070 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -147,3 +147,9 @@ Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x Fail Check {x@{u},y|x=x}. Fail Check {?[n],y|0=0}. + +(* Check that 10 is well declared left associative *) + +Section C. +Notation "f $$$ x" := (id f x) (at level 10, left associativity). +End C. |