Commit 5b22c4cf authored by Ralf Jung's avatar Ralf Jung

make it all compile with an opaque world-prop

parent 758ad9f5
......@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile lib/ModuRes -R lib/ModuRes ModuRes core_lang.v iris.v iris_core.v lang.v masks.v world_prop.v world_prop_old.v world_prop_sig.v -o Makefile
# coq_makefile lib/ModuRes -R lib/ModuRes ModuRes core_lang.v iris.v iris_core.v lang.v masks.v world_prop.v world_prop_sig.v -o Makefile
#
.DEFAULT_GOAL := all
......@@ -82,11 +82,10 @@ endif
VFILES:=core_lang.v\
iris.v\
# iris_core.v\
iris_core.v\
lang.v\
masks.v\
world_prop.v\
world_prop_old.v\
world_prop_sig.v
-include $(addsuffix .d,$(VFILES))
......
......@@ -25,7 +25,6 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
Instance Props_BI : ComplBI Props | 0 := _.
Instance Props_Later : Later Props | 0 := _.
Set Printing All.
(** And now we're ready to build the IRIS-specific connectives! *)
......
......@@ -5,7 +5,7 @@ Require Import ModuRes.Finmap ModuRes.Constr.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI.
Require Import world_prop_sig.
Module WorldProp (Res : PCM_T) <: WORLD_PROP Res.
Module WorldProp (Res : PCM_T) : WORLD_PROP Res.
(** The construction is parametric in the monoid we choose *)
Import Res.
......
......@@ -20,7 +20,7 @@ Module Type WORLD_PROP (Res : PCM_T).
Parameter ı : PreProp -t> halve (cmfromType Props).
Parameter ı' : halve (cmfromType Props) -t> PreProp.
Axiom iso : forall P, ı' (ı P) == P.
Axiom isoR : forall T, ı (ı' T) == T.
Axiom isoR: forall T, ı (ı' T) == T.
(* Define all the things on Props, so they have names - this shortens the terms later *)
Instance Props_ty : Setoid Props := _.
......
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