diff options
| author | Maxime Dénès | 2017-11-29 12:56:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-29 12:56:44 +0100 |
| commit | 28dabf726be49bd47538642d1bae83990def4236 (patch) | |
| tree | de3c41e16b7864b8875ad77796911fb63e87b11d | |
| parent | 5109763ca7d2a1469b392b271da7c1ed711d4258 (diff) | |
| parent | 7d0eb42050cb4f75c95cefb11c0cac5efa32f40a (diff) | |
Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of levels
| -rw-r--r-- | parsing/egramcoq.ml | 5 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 9 | ||||
| -rw-r--r-- | test-suite/success/Notations.v | 6 |
3 files changed, 12 insertions, 8 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 2cb7da5694..9c2766187e 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; @@ -46,8 +46,7 @@ let default_pattern_levels = 100,Extend.RightA,false; 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..7e5933cea2 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -377,11 +377,10 @@ GEXTEND Gram [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] - | "11" LEFTA + | "10" LEFTA [ p = pattern; "as"; id = ident -> - CAst.make ~loc:!@loc @@ CPatAlias (p, id) ] - | "10" RIGHTA - [ p = pattern; lp = LIST1 NEXT -> + CAst.make ~loc:!@loc @@ CPatAlias (p, id) + | p = pattern; lp = LIST1 NEXT -> (let open CAst in match p with | { v = CPatAtom (Some r) } -> CAst.make ~loc:!@loc @@ CPatCstr (r, None, lp) | { v = CPatCstr (r, None, l2); loc } -> @@ -392,7 +391,7 @@ GEXTEND Gram | _ -> CErrors.user_err ?loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern" (Pp.str "Such pattern cannot have arguments.")) - |"@"; r = Prim.reference; lp = LIST0 NEXT -> + | "@"; r = Prim.reference; lp = LIST0 NEXT -> CAst.make ~loc:!@loc @@ CPatCstr (r, Some lp, []) ] | "1" LEFTA [ c = pattern; "%"; key=IDENT -> CAst.make ~loc:!@loc @@ CPatDelimiters (key,c) ] 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. |