Commit e0ed90f7 authored by Ralf Jung's avatar Ralf Jung

update std++

parent 5334813e
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 6ffa20c8f23797f81f1bb55ab27432e897de71d5
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 0ac2b4db07bdc471421c5a4c47789087b3df074c
......@@ -46,7 +46,7 @@ Section core.
Proof.
split.
- iIntros (HP) "HP". iDestruct (coreP_intro with "HP") as "#HcP".
iClear "∗". iAlways. by iApply HP.
iAlways. by iApply HP.
- iIntros (HPQ) "HcP". iDestruct (coreP_mono _ _ HPQ with "HcP") as "HcQ".
iDestruct (coreP_elim with "HcQ") as "#HQ". done.
Qed.
......
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