Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit ffa94a95 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Update to recent Iris.

parent ed4ac088
......@@ -11,6 +11,6 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris_time" ]
depends: [
"coq" { (>= "8.10.2" & < "8.13~") | (= "dev") }
"coq-iris" { (= "dev.2020-10-21.1.4b3d541a") | (= "dev") }
"coq-iris" { (= "dev.2020-11-13.0.88773f25") | (= "dev") }
"coq-tlc" { (= "20200328") | (= "dev") }
]
......@@ -18,7 +18,7 @@ Definition heap_adequacy Σ `{heapPreG Σ} s e σ φ :
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (??) "".
iMod (gen_heap_init σ) as (?) "Hh".
iMod (gen_heap_init σ) as (?) "[Hh _]".
iModIntro.
iExists (λ σ κs, (gen_heap_interp σ)%I), (λ _, True%I). iFrame.
iApply (Hwp (HeapG _ _ _)).
......
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