Skip to content
Snippets Groups Projects
Commit c80a25c4 authored by Simon Spies's avatar Simon Spies
Browse files

cleanup

parent 80447354
No related branches found
No related tags found
No related merge requests found
...@@ -212,7 +212,7 @@ Lemma marked_was_unmarked (G : Gmon) x v : ...@@ -212,7 +212,7 @@ Lemma marked_was_unmarked (G : Gmon) x v :
Proof. Proof.
intros H2; specialize (H2 x). intros H2; specialize (H2 x).
revert H2; rewrite lookup_op lookup_singleton. intros H2. revert H2; rewrite lookup_op lookup_singleton. intros H2.
by rewrite (excl_validN_inv_l 0 _ _ (proj1 (cmra_valid_validN _) H2 0)). by rewrite (excl_validN_inv_l O _ _ (proj1 (cmra_valid_validN _) H2 O)).
Qed. Qed.
Lemma mark_update_lookup_base (G : Gmon) x v : Lemma mark_update_lookup_base (G : Gmon) x v :
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment