Skip to content
Snippets Groups Projects
Commit 9aeb8f2b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris and remove a FIXME.

parent 3c5e3622
No related branches found
No related tags found
No related merge requests found
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9ea6fa453f1b9ef1cd4b5b8a167d1fab717c895e
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq f1b30a2eb12d38bffd8a0aa541c90e3675af2a29
......@@ -25,9 +25,7 @@ Section specs.
iIntros (? Φ) "HΦ". wp_lam. wp_op; intros ?.
- wp_if. assert (n = 0) as -> by lia. iApply ("HΦ" $! _ []).
rewrite heap_mapsto_vec_nil. auto.
- wp_if. wp_alloc l vl as "H↦" "H†".
(* FIXME: I have to state the coercion vec_to_list explicitly here. *)
iApply ("HΦ" $! _ (vec_to_list vl)).
- wp_if. wp_alloc l vl as "H↦" "H†". iApply ("HΦ" $! _ vl).
rewrite vec_to_list_length -{2}Hsz Z2Nat.id //. iFrame. auto.
Qed.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment