diff --git a/Makefile b/Makefile
index 02790ecc117c7d941bb0d90662edbb95ee0362aa..4812b97791ffd22a860951c66253f67ce9c12cb1 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 ba8473549d0ac5bf459fe204c5dd08565ac0f3cb..4596631efcd4b02ef0d9a18f90d04542cc3fe5cc 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 7fd476ad5c611934141e1b7dfffb43619798e332..5f12e852f9659384665677391d079cd025475754 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 2f45c590302a1cb9f4c510e61f1e98564795fc61..5399a01ca37e54d45162d15537889b5fe0514644 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 := _.