Skip to content
Snippets Groups Projects
Verified Commit e40374b8 authored by Johannes Hostert's avatar Johannes Hostert
Browse files

Make dyn_reservation_map follow style for updateP

parent 0a7d4889
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
iris/algebra/dyn_reservation_map.v
+ 1
− 1
View file @ e40374b8
......@@ -298,7 +298,7 @@ Section cmra.
apply elem_of_dom_2, elem_of_gset_to_coPset in Hp. right. set_solver.
Qed.
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.
Proof. eauto using dyn_reservation_map_reserve. Qed.
Lemma dyn_reservation_map_alloc E k a :
......
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