Commit 7279eda4 authored by Ralf Jung's avatar Ralf Jung

Revert "IrisRes no longer hides core resource and language types.": it's not actually needed

This reverts commit 608fe86e22b912d9d591cd2d0c4e2943b1abe6ce.
parent 37923961
Require Import world_prop core_lang lang masks. Require Import world_prop core_lang lang masks.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap. Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
Module Type IRIS_RES (RL : PCM_T) (C : CORE_LANG) := Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T.
PCM_T with Definition res := (pcm_res_ex C.state * RL.res)%type. Import C.
Definition res := (pcm_res_ex 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_op : PCM_op res := _.
Instance res_unit : PCM_unit res := _. Instance res_unit : PCM_unit res := _.
Instance res_pcm : PCM res := _. Instance res_pcm : PCM res := _.
......
Markdown is supported
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