Verified Commit 76cbd20a authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Workaround Coq bug #14441

parent a806150e
......@@ -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.
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment