Commit d8965431 authored by Robbert Krebbers's avatar Robbert Krebbers

Solve atomic obligations also by "assumption".

parent 37cf94e2
Pipeline #2954 passed with stage
in 9 minutes and 53 seconds
......@@ -314,3 +314,5 @@ Section proofmode_classes.
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
End proofmode_classes.
Hint Extern 0 (atomic _) => assumption : typeclass_instances.
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