diff options
| author | Hugo Herbelin | 2017-11-26 19:18:38 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-27 11:27:34 +0100 |
| commit | 134b220b77d74b0ada801d215a2e5c66bc6726ea (patch) | |
| tree | 27889d694009730a3fd0db51587b95c725fa26c4 | |
| 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).
| -rw-r--r-- | parsing/egramcoq.ml | 4 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 2 | ||||
| -rw-r--r-- | test-suite/success/Notations.v | 6 |
3 files changed, 9 insertions, 3 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 2cb7da5694..acbe2d982d 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -35,7 +35,7 @@ let default_levels = 100,Extend.RightA,false; 99,Extend.RightA,true; 90,Extend.RightA,true; - 10,Extend.RightA,false; + 10,Extend.LeftA,false; 9,Extend.RightA,false; 8,Extend.RightA,true; 1,Extend.LeftA,false; @@ -47,7 +47,7 @@ let default_pattern_levels = 99,Extend.RightA,true; 90,Extend.RightA,true; 11,Extend.LeftA,false; - 10,Extend.RightA,false; + 10,Extend.LeftA,false; 1,Extend.LeftA,false; 0,Extend.RightA,false] diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 844c040fdf..bfebca2a5c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -380,7 +380,7 @@ GEXTEND Gram | "11" LEFTA [ p = pattern; "as"; id = ident -> CAst.make ~loc:!@loc @@ CPatAlias (p, id) ] - | "10" RIGHTA + | "10" LEFTA [ p = pattern; lp = LIST1 NEXT -> (let open CAst in match p with | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp) diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index e3f90f6d94..3c0ad20700 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. |