diff options
| author | Hugo Herbelin | 2020-07-15 13:07:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-07-15 18:08:00 +0200 |
| commit | fff15259300b42d83e0d135aa3abc10f274f719d (patch) | |
| tree | acd127e09eae048032b38db3bfe2e960c566c326 /test-suite | |
| parent | 33e748514dad9459885006a1523d107d556be22b (diff) | |
Fix bug #12691 (an only parsing notation induces a generic printing format).
This is to anticipate further not-only-parsing uses of the notation.
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. |