make things compile reasonably fast

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!
   
 
 

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.