Skip to content

GitLab

Commit 8ce92349 authored by Ralf Jung's avatar Ralf Jung
Browse files

fix accidental use of coPset domain

parent bc1afae4
Pipeline #65646 passed with stage
in 7 minutes and 40 seconds
Hide whitespace changes
Inline Side-by-side
iris/algebra/dyn_reservation_map.v
View file @ 8ce92349
...@@ -294,7 +294,7 @@ Section cmra. ...@@ -294,7 +294,7 @@ Section cmra.
- eapply set_infinite_subseteq, HE2inf. set_solver. - eapply set_infinite_subseteq, HE2inf. set_solver.
- intros i. rewrite left_id_L. destruct (Hdisj i) as [?|Hi]; first by left. - intros i. rewrite left_id_L. destruct (Hdisj i) as [?|Hi]; first by left.
destruct (mf !! i) as [p|] eqn:Hp; last by left. destruct (mf !! i) as [p|] eqn:Hp; last by left.
apply (elem_of_dom_2 (D:=coPset)) in Hp. right. set_solver. apply (elem_of_dom_2 (D:=gset _)), elem_of_gset_to_coPset in Hp. right. set_solver.
Qed. Qed.
Lemma dyn_reservation_map_reserve' : Lemma dyn_reservation_map_reserve' :
ε ~~>: (λ x, ∃ E, set_infinite E ∧ x = dyn_reservation_map_token E). ε ~~>: (λ x, ∃ E, set_infinite E ∧ x = dyn_reservation_map_token E).
......
Supports Markdown
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