diff --git a/tests/notation.ref b/tests/notation.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/notation.v b/tests/notation.v
new file mode 100644
index 0000000000000000000000000000000000000000..d1ded9f628942ecd1a21b6b241963547653748a9
--- /dev/null
+++ b/tests/notation.v
@@ -0,0 +1,9 @@
+From stdpp Require Import base tactics.
+
+(** Test parsing of variants of [(≡)] notation. *)
+Lemma test_equiv_annot_sections `{!Equiv A, Equivalence A (≡@{A})} (x : A) :
+  x ≡@{A} x ∧ (≡@{A}) x x ∧ (x ≡.) x ∧ (.≡ x) x ∧
+  ((x ≡@{A} x)) ∧ ((≡@{A})) x x ∧ ((x ≡.)) x ∧ ((.≡ x)) x ∧
+  ( x ≡@{A} x) ∧ ( x ≡.) x ∧
+  (x ≡@{A} x ) ∧ (≡@{A} ) x x ∧ (.≡ x ) x.
+Proof. naive_solver. Qed.