From 7279eda4d4b014b2abb69ed28aa09833f7a560c7 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 5 Feb 2015 15:12:06 +0100 Subject: [PATCH] Revert "IrisRes no longer hides core resource and language types.": it's not actually needed This reverts commit 608fe86e22b912d9d591cd2d0c4e2943b1abe6ce. --- iris_core.v | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/iris_core.v b/iris_core.v index b003297f..6d2a8e2d 100644 --- a/iris_core.v +++ b/iris_core.v @@ -1,11 +1,9 @@ Require Import world_prop core_lang lang masks. Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap. -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. +Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T. + Import C. + Definition res := (pcm_res_ex state * RL.res)%type. Instance res_op : PCM_op res := _. Instance res_unit : PCM_unit res := _. Instance res_pcm : PCM res := _. -- GitLab