From 5b22c4cf0c2311abb57a312b01c5850f5d3f5ffd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 1 Feb 2015 13:30:24 +0100
Subject: [PATCH] make it all compile with an opaque world-prop

---
 Makefile         | 5 ++---
 iris.v           | 1 -
 world_prop.v     | 2 +-
 world_prop_sig.v | 2 +-
 4 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/Makefile b/Makefile
index 02790ecc1..4812b9779 100644
--- a/Makefile
+++ b/Makefile
@@ -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))
diff --git a/iris.v b/iris.v
index ba8473549..4596631ef 100644
--- a/iris.v
+++ b/iris.v
@@ -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! *)
 
diff --git a/world_prop.v b/world_prop.v
index 7fd476ad5..5f12e852f 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -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.
diff --git a/world_prop_sig.v b/world_prop_sig.v
index 2f45c5903..5399a01ca 100644
--- a/world_prop_sig.v
+++ b/world_prop_sig.v
@@ -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 := _.
-- 
GitLab