Verified Commit 51362a58 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Needed fix (bug?)

parent a806150e
Pipeline #48931 failed with stage
in 9 minutes and 52 seconds
......@@ -171,7 +171,7 @@ 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).
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 +324,7 @@ 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).
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.
......
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