Commit 53c1d450 authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Small tweaks

parent 3ebef6ab
Pipeline #51507 passed with stage
in 9 minutes and 19 seconds
......@@ -72,7 +72,7 @@ Coq 8.11 is no longer supported in this version of Iris.
* Slight change to the `AACC` notation for atomic accessors (which is usually
only printed, not parsed): added a `,` before `ABORT`, for consistency with `COMM`.
* Add the lemmas `big_sepM_impl_strong` and `big_sepM_impl_dom_subseteq` that
generalize the existing `big_sepM_impl` lemma.
generalize the existing `big_sepM_impl` lemma. (by Simon Friis Vindum)
**Changes in `proofmode`:**
......@@ -1543,6 +1543,7 @@ Proof.
rewrite pure_True // left_id // wand_elim_l //.
Lemma big_sepM_impl_dom_subseteq `{Countable K} {A B}
(Φ : K A PROP) (Ψ : K B PROP) (m1 : gmap K A) (m2 : gmap K B) :
dom (gset _) m2 dom _ m1
([ map] kx m1, Φ k x) -
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