Commit 06c98c0f authored by Michael Sammler's avatar Michael Sammler
Browse files

update Iris

parent 313b5c0d
Pipeline #48103 failed with stage
in 15 minutes and 6 seconds
......@@ -17,7 +17,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
depends: [
"coq" { (>= "8.12.0" & < "8.13~") }
"coq-iris" { (= "dev.2021-04-22.0.dea10729") | (= "dev") }
"coq-iris" { (= "dev.2021-06-03.4.27c78b61") | (= "dev") }
"dune" {>= "2.7.0"}
"cerberus" {= "~dev"}
"cmdliner" {>= "1.0.4"}
......
......@@ -7,11 +7,11 @@ Set Default Proof Using "Type".
Import uPred.
Class refinedcG Σ := RefinedCG {
refinedcG_invG : invG Σ;
refinedcG_invG : invGS Σ;
refinedcG_gen_heapG :> heapG Σ
}.
Instance c_irisG `{!refinedcG Σ} : irisG c_lang Σ := {
Instance c_irisG `{!refinedcG Σ} : irisGS c_lang Σ := {
iris_invG := refinedcG_invG;
state_interp σ κs _ _ := state_ctx σ;
fork_post _ := True%I;
......
......@@ -8,7 +8,7 @@ From iris.program_logic Require Export language.
Set Default Proof Using "Type".
Class typePreG Σ := PreTypeG {
type_invG :> invPreG Σ;
type_invG :> invGpreS Σ;
type_heap_heap_inG :> inG Σ (authR heapUR);
type_heap_alloc_range_map_inG :> ghost_mapG Σ alloc_id (Z * nat);
type_heap_alloc_alive_map_inG :> ghost_mapG Σ alloc_id bool;
......
Supports Markdown
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