diff options
| author | Ralf Jung | 2017-02-14 12:35:39 +0100 |
|---|---|---|
| committer | Ralf Jung | 2017-02-16 16:46:41 +0100 |
| commit | 55cb913f029308e97bd262fc18d4338f404e7561 (patch) | |
| tree | 3152c0912430102a15f1a22e5d69631431d92961 /test-suite | |
| parent | 29d7872c0159d2aab7264c0577a2f5a9dc7c90c9 (diff) | |
don't require printing-only notation to be productive
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Notations.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 07bbb60c40..32baeaa570 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -128,3 +128,7 @@ Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). Goal True. {{ exact I. }} Qed. + +(* Check that we can have notations without any symbol iff they are "only printing". *) +Fail Notation "" := (@nil). +Notation "" := (@nil) (only printing). |