Commit 5cdc535e authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 803e6561
Pipeline #12767 passed with stage
in 9 minutes and 17 seconds
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [
"coq-iris" { (= "dev.2018-10-31.4.4a1eb8a3") | (= "dev") }
"coq-iris" { (= "dev.2018-11-08.2.9eee9408") | (= "dev") }
]
......@@ -84,7 +84,7 @@ Section proofs.
- wp_op. wp_if. wp_apply new_list_spec; first done.
iIntros (v) "Hl"; by iApply "HΦ".
- intros n'. wp_op. wp_if.
rewrite Zpos_P_of_succ_nat. wp_op. rewrite Z.sub_1_r -Zpred_succ.
rewrite Nat2Z.inj_succ. wp_op. rewrite Z.sub_1_r Z.pred_succ.
wp_apply ("IH" $! n'); first done.
iIntros (l) "Hl".
wp_let.
......
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