From ac3ddfda2182e29f273b59a9a48fcdabb412b794 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 15 Jun 2021 08:55:04 +0200
Subject: [PATCH] Add suggested test

---
 tests/algebra.v | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/tests/algebra.v b/tests/algebra.v
index ec82c5740..5399a0069 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,6 +1,34 @@
 From iris.algebra Require Import auth excl lib.gmap_view.
 From iris.base_logic.lib Require Import invariants.
 
+Section test_dist_equiv_mode.
+  Local Unset Mangle Names.
+  (* check that the mode for [Dist] does not trigger https://github.com/coq/coq/issues/14441.
+  From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
+
+  (* succeeds *)
+  Lemma list_dist_lookup {A : ofe} n (l1 l2 : list A) :
+    l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
+  Abort.
+  Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) :
+    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
+  Abort.
+  Lemma list_equiv_lookup_equiv `{Equiv A} (l1 l2 : list A) :
+    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
+  Abort.
+
+  Local Hint Mode Equiv ! : typeclass_instances.
+
+  (* succeeds *)
+  Lemma list_equiv_lookup_ofe {A : ofe} (l1 l2 : list A) :
+    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
+  Abort.
+
+  (* fails *)
+  Fail Lemma list_equiv_lookup_equiv `{Equiv A} (l1 l2 : list A) :
+    l1 ≡ l2 ↔ ∀ i, l1 !! i ≡ l2 !! i.
+End test_dist_equiv_mode.
+
 (** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
 with carriers that are definitionally equal. See also
 https://gitlab.mpi-sws.org/iris/iris/issues/299 *)
-- 
GitLab