diff options
| -rw-r--r-- | parsing/lexer.ml4 | 6 | ||||
| -rw-r--r-- | test-suite/success/Notations.v | 6 |
2 files changed, 12 insertions, 0 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 5d96873f31..db6816a704 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -535,6 +535,12 @@ let rec next_token = parser bp next_token s | [< t = process_chars bp c >] -> comment_stop bp; t >] -> t + | [< ' ('{' | '}' as c); s >] ep -> + let t,new_between_com = + if !between_com then (KEYWORD (String.make 1 c), (bp, ep)), true + else process_chars bp c s,false + in + comment_stop bp; between_com := new_between_com; t | [< s >] -> match lookup_utf8 s with | Utf8Token (Unicode.Letter, n) -> diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 2f7c62972a..511b60b4bb 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -110,3 +110,9 @@ Goal True -> True. intros H. exact H. Qed. (* Check absence of collision on ".." in nested notations with ".." *) Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). + +(* Check parsing of { and } is not affected by notations #3479 *) +Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). +Goal True. +{{ exact I. }} +Qed. |