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