diff --git a/README.txt b/README.txt
index b73d8cffcffd057572fbe2dc1369b391cfa9e02d..2711252f4ae6f2345d1ba8ae98d30440dd15fe3b 100644
--- a/README.txt
+++ b/README.txt
@@ -71,20 +71,16 @@ REQUIREMENTS
   8GB ram + 4GB swap
 
   We have tested the development using Coq v. 8.4pl4 on Linux and Mac
-  machines with at least 8GB RAM + 4GB swap.  The entire compilation
-  took around 3 hours.
+  machines.  The entire compilation took less than 30 minutes.
   
 
 HOW TO COMPILE
 
   To compile the development, run
   
-  > make 
+  > make -j
 
   in the folder containing this README. 
-
-  Be aware that iris.v takes a long time to check and needs
-  significant amounts of RAM!
   
 
 
diff --git a/world_prop.v b/world_prop.v
index 103ead16f7dcdb3ce68d72f51269dc7cd6bec61e..963f23685978ef8a00b6d8302411379b69d39f0c 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -80,8 +80,19 @@ Module WorldProp (Res : PCM_T).
   Lemma isoR T : ı (ı' T) == T.
   Proof. apply (UF_id T). Qed.
 
+  (* PreProp has an equivalence and a complete metric. It also has a preorder that fits to everything else. *)
+  Instance PProp_ty   : Setoid PreProp     := _.
+  Instance PProp_m    : metric PreProp     := _.
+  Instance PProp_cm   : cmetric PreProp    := _.
   Instance PProp_preo : preoType PreProp   := disc_preo PreProp.
   Instance PProp_pcm  : pcmType PreProp    := disc_pcm PreProp.
   Instance PProp_ext  : extensible PreProp := disc_ext PreProp.
 
+  (* Give names to the things for Props, so the terms can get shorter. *)
+  Instance Props_ty   : Setoid Props     := _.
+  Instance Props_m    : metric Props     := _.
+  Instance Props_cm   : cmetric Props    := _.
+  Instance Props_preo : preoType Props   := _.
+  Instance Props_pcm  : pcmType Props    := _.
+
 End WorldProp.