Commit 6d778c56 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent aadb3dfd
Pipeline #28577 passed with stage
in 21 minutes and 50 seconds
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [ depends: [
"coq-iris" { (= "dev.2020-04-16.1.4b6f5dc6") | (= "dev") } "coq-iris" { (= "dev.2020-05-13.0.635cdf1e") | (= "dev") }
] ]
...@@ -59,7 +59,7 @@ Section gcd_spec. ...@@ -59,7 +59,7 @@ Section gcd_spec.
iInduction (lt_wf b) as [[|b] _] "IH" forall (a). iInduction (lt_wf b) as [[|b] _] "IH" forall (a).
{ vcg. iIntros "!> !> **". rewrite Nat.gcd_0_r. iFrame. } { vcg. iIntros "!> !> **". rewrite Nat.gcd_0_r. iFrame. }
vcg. iIntros "!> !>" (t) "!> **". vcg. iIntros "!> !>" (t) "!> **".
rewrite Z.rem_mod_nonneg; [|lia..]; rewrite -Z2Nat_inj_mod. rewrite Z.rem_mod_nonneg; [|lia..]; rewrite -Nat2Z_inj_mod.
iApply (cwp_wand with "(IH [%] [$] [$])"); [by apply Nat.mod_upper_bound|]. iApply (cwp_wand with "(IH [%] [$] [$])"); [by apply Nat.mod_upper_bound|].
iIntros (v) "[??]". rewrite Nat.gcd_comm Nat.gcd_mod // Nat.gcd_comm. iIntros (v) "[??]". rewrite Nat.gcd_comm Nat.gcd_mod // Nat.gcd_comm.
vcg_continue. auto with iFrame. vcg_continue. auto with iFrame.
......
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