diff options
| author | Emilio Jesus Gallego Arias | 2020-07-21 15:17:32 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-21 15:17:32 +0200 |
| commit | 8f4d7ddf4c3736a190b3e073fadb844c017628d3 (patch) | |
| tree | 54b6ff9f33a174f60f3dc431ac6c2a677ac3395a /test-suite | |
| parent | f44202e28f38aa900801b0c90514690b6a401bed (diff) | |
| parent | fff15259300b42d83e0d135aa3abc10f274f719d (diff) | |
Merge PR #12697: Fix bug #12691: an only-parsing notation needs to produce a generic printing format in anticipation of further not-only-parsing uses of the notation
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Notations4.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 8 |
2 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 9cb019ca56..fa03ec8193 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -119,3 +119,7 @@ fun x : nat => V x : forall x : nat, nat * (?T -> ?T) where ?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) +File "stdin", line 297, characters 0-30: +Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] +0 :=: 0 + : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index b3270d4f92..90d8da2bec 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -290,3 +290,11 @@ Check V tt. Check fun x : nat => V x. End O. + +Module Bug12691. + +Notation "x :=: y" := True (at level 70, no associativity, only parsing). +Notation "x :=: y" := (x = y). +Check (0 :=: 0). + +End Bug12691. |