diff options
| author | Hugo Herbelin | 2016-10-24 17:04:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-24 17:11:28 +0200 |
| commit | 5f1dd4c401110d6b10350c847805c6923fa09de5 (patch) | |
| tree | 1f72c8426bb48e504dacf1f556427557594662df | |
| parent | 1d769e02b3baba54246c942fe116abaf850892db (diff) | |
Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{" or "}").
| -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. |