From bd9d16c9ae260ad90f3e5708507a9f0bece51d82 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 18 Jun 2021 08:48:34 +0200
Subject: [PATCH] don't test 'Hint Mode Equiv !'; wait for Coq fix instead

---
 tests/algebra.v | 17 +----------------
 1 file changed, 1 insertion(+), 16 deletions(-)

diff --git a/tests/algebra.v b/tests/algebra.v
index 5460faec3..c9f46319f 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -2,35 +2,20 @@ 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.
+
   (* analogous test for [Equiv] and https://github.com/coq/coq/issues/14441.
   From https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/700#note_69303. *)
-
   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 due to https://github.com/coq/coq/issues/14441; commented out, hoping
-  for a fix in Coq. *)
-  (* 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
-- 
GitLab