From bf052ca15c0358c659b9aa8d9b199739143505e0 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 2 Jul 2023 16:28:34 +0200
Subject: [PATCH] Test problem with monotone cmra

---
 tests/monotone.ref |  0
 tests/monotone.v   | 14 ++++++++++++++
 2 files changed, 14 insertions(+)
 create mode 100644 tests/monotone.ref
 create mode 100644 tests/monotone.v

diff --git a/tests/monotone.ref b/tests/monotone.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/monotone.v b/tests/monotone.v
new file mode 100644
index 000000000..b5e65ef77
--- /dev/null
+++ b/tests/monotone.v
@@ -0,0 +1,14 @@
+Require Import iris.unstable.algebra.monotone.
+
+Section test_mra_over_ofe.
+  Context {A : ofe} {R : relation A}.
+  Implicit Types a b : A.
+  Implicit Types x y : mra R.
+
+  Context `{!Reflexive R} {Has : AntiSymm (≡) R}.
+  Lemma test a b : principal R a ≡ principal R b → a ≡ b.
+  Proof.
+    Fail by intros ?%(inj _).
+    by intros ?%(inj (R := equiv) _).
+  Qed.
+End test_mra_over_ofe.
-- 
GitLab