From 473e5f3cfcbeb85ead718ef1a16ce00f136c137c Mon Sep 17 00:00:00 2001 From: David Swasey <swasey@mpi-sws.org> Date: Thu, 5 Feb 2015 07:41:05 +0100 Subject: [PATCH] IrisRes no longer hides core resource and language types. --- iris_core.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/iris_core.v b/iris_core.v index d2f8e2586..a9919b841 100644 --- a/iris_core.v +++ b/iris_core.v @@ -1,9 +1,11 @@ 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 := _. -- GitLab