Commit a4237b93 authored by Ralf Jung's avatar Ralf Jung

fix for Iris bump

parent bb62b280
Pipeline #6769 passed with stage
in 14 minutes and 48 seconds
......@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
"coq-iris" { (= "dev.2018-01-21.0") | (= "dev") }
"coq-iris" { (= "dev.2018-02-09.0") | (= "dev") }
]
......@@ -26,7 +26,7 @@ Section specs.
- wp_if. assert (n = 0) as -> by lia. iApply "HΦ".
rewrite heap_mapsto_vec_nil. auto.
- wp_if. wp_alloc l as "H↦" "H†". omega. iApply "HΦ". subst sz.
iFrame. auto.
iFrame.
Qed.
Lemma wp_delete E (n:Z) l vl :
......
......@@ -820,7 +820,7 @@ Section arc.
{ destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
iDestruct "H↦" as (vl) "[? Heq]". iDestruct "Heq" as %<-.
wp_apply (wp_delete _ _ _ (_::_::vl) with "[-]"); [simpl;lia| |done].
rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. auto. }
rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. }
iIntros (?) "_". wp_seq.
(* Finish up the proof. *)
iApply (type_type _ _ _ [ rcx box (uninit 1); r box (uninit 0) ]
......@@ -884,7 +884,7 @@ Section arc.
{ destruct b; wp_if=>//. iDestruct "Hdrop" as "((? & H↦) & ? & ?)".
iDestruct "H↦" as (vl') "[? Heq]". iDestruct "Heq" as %<-.
wp_apply (wp_delete _ _ _ (_::_::vl') with "[-]"); [simpl; lia| |done].
rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. auto. }
rewrite !heap_mapsto_vec_cons shift_loc_assoc. iFrame. }
iIntros (?) "_". wp_seq.
iApply (type_type _ _ _ [ rcx box (uninit 1); #r box (Σ[ ty; arc ty ]) ]
with "[] LFT HE Hna HL Hk [-]"); last first.
......
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