Merge branch 'master' of git.fp.mpi-sws.org:nowbook

README.txt

@@ -56,7 +56,7 @@ CONTENTS
   * world_prop.v uses the ModuRes Coq library to construct the domain
     for Iris propositions
   
-  * iris_core.v defines erasure and the simpler assertions
+  * iris_core.v defines world satisfaction and the simpler assertions
   
   * iris_vs.v defines view shifts and proves their rules
   

iris_core.v

 Require Import world_prop core_lang lang masks.
 Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
 
-Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T.
-  Import C.
-  Definition res := (pcm_res_ex state * RL.res)%type.
+Module Type IRIS_RES (RL : PCM_T) (C : CORE_LANG) :=
+  PCM_T with Definition res := (pcm_res_ex C.state * RL.res)%type.
+
+Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: IRIS_RES RL C.
+  Definition res := (pcm_res_ex C.state * RL.res)%type.
   Instance res_op   : PCM_op res := _.
   Instance res_unit : PCM_unit res := _.
   Instance res_pcm  : PCM res := _.