From f5ed12e195e5835c09a64c5eff89caf2084ce565 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 10 Apr 2020 01:42:49 +0200
Subject: [PATCH] Add tests for equiv notation

Extracted from https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/409.
---
 tests/notation.ref | 0
 tests/notation.v   | 9 +++++++++
 2 files changed, 9 insertions(+)
 create mode 100644 tests/notation.ref
 create mode 100644 tests/notation.v

diff --git a/tests/notation.ref b/tests/notation.ref
new file mode 100644
index 00000000..e69de29b
diff --git a/tests/notation.v b/tests/notation.v
new file mode 100644
index 00000000..d1ded9f6
--- /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.
-- 
GitLab