From 25feff74476519b15014252022a42960687d668f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Jun 2015 19:53:56 +0200
Subject: [PATCH] make things compile reasonably fast

---
 README.txt   |  8 ++------
 world_prop.v | 11 +++++++++++
 2 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/README.txt b/README.txt
index b73d8cffc..2711252f4 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 103ead16f..963f23685 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.
-- 
GitLab