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.