diff --git a/opam b/opam index b376f16b3f7b699f944351cb7f69d85ae495b7a3..a126d503c8c6a1f3efdc8f39b040294290028263 100644 --- a/opam +++ b/opam @@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] install: [make "install"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"] depends: [ - "coq-iris-heap-lang" { (= "dev.2021-05-26.5.13d5ab4f") | (= "dev") } + "coq-iris-heap-lang" { (= "dev.2021-06-03.0.2959900d") | (= "dev") } "coq-autosubst" { = "dev" } ] diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v index 236458cf410f0f591353c1b45b9e64ec833628c4..d00cf9bfc15382bc5a0f2e7586d581e5e57b48c4 100644 --- a/theories/logic/adequacy.v +++ b/theories/logic/adequacy.v @@ -6,7 +6,7 @@ From iris.heap_lang Require Export adequacy. From reloc.logic Require Export spec_ra model. Class relocPreG Σ := RelocPreG { - reloc_preG_heap :> heapPreG Σ; + reloc_preG_heap :> heapGpreS Σ; reloc_preG_cfg :> inG Σ (authR cfgUR) }. diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v index 57890b9782e97fb6dfc716cf7a097ebac1d02ee2..bf0a45ace2882c1aebd202760d0afe6df1455d65 100644 --- a/theories/logic/spec_ra.v +++ b/theories/logic/spec_ra.v @@ -19,7 +19,7 @@ Definition cfgUR := prodUR tpoolUR (heapUR loc (option val)). (** The CMRA for the thread pool. *) Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }. Class relocG Σ := RelocG { - relocG_heapG :> heapG Σ; + relocG_heapG :> heapGS Σ; relocG_cfgG :> cfgSG Σ; }. @@ -28,7 +28,7 @@ Definition to_heap {L V} `{Countable L} : gmap L V → heapUR L V := Definition to_tpool (tp : list expr) : tpoolUR := Excl <$> (map_seq 0 tp). Section definitionsS. - Context `{cfgSG Σ, invG Σ}. + Context `{cfgSG Σ, invGS Σ}. Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ := own cfg_name (◯ (∅, {[ l := (q, to_agree (Some v)) ]})).