Merge branch 'modes-broken' into 'master'

Modes for Equiv

See merge request iris/iris!701

CHANGELOG.md

@@ -33,6 +33,9 @@ Coq 8.11 is no longer supported in this version of Iris.
   algorithm.
 * Set `Hint Mode` for the classes `OfeDiscrete`, `Dist`, `Unit`, `CmraMorphism`,
   `rFunctorContractive`, `urFunctorContractive`.
+* Set `Hint Mode` for the stdpp class `Equiv`. This might require few spurious
+  type annotations until
+  [Coq bug #14441](https://github.com/coq/coq/issues/14441) is fixed.
 * Add `max_prefix_list` RA on lists whose composition is only defined when one
   operand is a prefix of the other. The result is the longer list.
 

iris/algebra/big_op.v

@@ -171,7 +171,8 @@ Section list.
     ([^o list] k ↦ y ∈ l1, f k y) ≡ ([^o list] k ↦ y ∈ l2, g k y).
   Proof.
     intros Hl Hf. apply big_opL_gen_proper_2; try (apply _ || done).
-    intros k. assert (l1 !! k ≡ l2 !! k) as Hlk by (by f_equiv).
+    (* FIXME (Coq #14441) unnecessary type annotation *)
+    intros k. assert (l1 !! k ≡@{option A} l2 !! k) as Hlk by (by f_equiv).
     destruct (l1 !! k) eqn:?, (l2 !! k) eqn:?; inversion Hlk; naive_solver.
   Qed.
 
@@ -324,7 +325,8 @@ Section gmap.
     ([^o map] k ↦ y ∈ m1, f k y) ≡ ([^o map] k ↦ y ∈ m2, g k y).
   Proof.
     intros Hl Hf. apply big_opM_gen_proper_2; try (apply _ || done).
-    intros k. assert (m1 !! k ≡ m2 !! k) as Hlk by (by f_equiv).
+    (* FIXME (Coq #14441) unnecessary type annotation *)
+    intros k. assert (m1 !! k ≡@{option A} m2 !! k) as Hlk by (by f_equiv).
     destruct (m1 !! k) eqn:?, (m2 !! k) eqn:?; inversion Hlk; naive_solver.
   Qed.
 

iris/prelude/prelude.v

@@ -7,3 +7,7 @@ Ltac done := stdpp.tactics.done.
 
 (** Iris itself and many dependencies still rely on this coercion. *)
 Coercion Z.of_nat : nat >-> Z.
+
+(* No Hint Mode set in stdpp because of Coq bugs #5735 and #9058, only
+fixed in Coq >= 8.12, which Iris depends on. *)
+Global Hint Mode Equiv ! : typeclass_instances.

tests/algebra.v

@@ -13,9 +13,6 @@ Section test_dist_equiv_mode.
   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.
 End test_dist_equiv_mode.
 
 (** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs