diff --git a/configure b/configure
new file mode 100755
index 0000000000000000000000000000000000000000..244a33b85db084aeb928420a6dfefd3c9b765901
--- /dev/null
+++ b/configure
@@ -0,0 +1,2 @@
+#!/bin/sh
+coq_makefile lib/ModuRes -R lib/ModuRes ModuRes *.v -o Makefile
diff --git a/iris.v b/iris.v
index ea1e11eb81243a1c8a4c6837b7dbc4a6bd080acd..125f4870787664d4f677e15fbd1dd35be405b3b5 100644
--- a/iris.v
+++ b/iris.v
@@ -25,7 +25,7 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
 
   Instance Props_BI : ComplBI Props | 0 := _.
   Instance Props_Later : Later Props | 0 := _.
-
+  
   (* Benchmark: How large is thid type? *)
   Section Benchmark.
     Local Open Scope mask_scope.
@@ -33,11 +33,12 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
     Local Open Scope bi_scope.
     Local Open Scope lang_scope.
 
-    Local Instance expr_type : Setoid expr := discreteType.
-    Local Instance expr_metr : metric expr := discreteMetric.
-    Local Instance expr_cmetr : cmetric expr := discreteCMetric.
+    Local Instance _bench_expr_type : Setoid expr := discreteType.
+    Local Instance _bench_expr_metr : metric expr := discreteMetric.
+    Local Instance _bench_cmetr : cmetric expr := discreteCMetric.
 
     Set Printing All.
+    Check (expr -n> (value -n> Props) -n> Props).
     Check ((expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props).
   End Benchmark.
 
@@ -403,6 +404,7 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
 
   End Erasure.
 
+  Check erasure.
 
   Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity).
 
@@ -484,6 +486,8 @@ Module Iris (RL : PCM_T) (C : CORE_LANG).
 
   End ViewShifts.
 
+  Check vs.
+
   Section ViewShiftProps.
     Local Open Scope mask_scope.
     Local Open Scope pcm_scope.
@@ -996,6 +1000,8 @@ Qed.
 
   End HoareTriples.
 
+  Check wp.
+
   Section Soundness.
     Local Open Scope mask_scope.
     Local Open Scope pcm_scope.
@@ -1211,6 +1217,8 @@ Qed.
 
   End Soundness.
 
+  Check soundness.
+
   Section HoareTripleProperties.
     Local Open Scope mask_scope.
     Local Open Scope pcm_scope.
diff --git a/world_prop.v b/world_prop.v
index 103ead16f7dcdb3ce68d72f51269dc7cd6bec61e..1466e8e12d9af83199d1ab3d9db03a2d39f64337 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -80,8 +80,20 @@ Module WorldProp (Res : PCM_T).
   Lemma isoR T : ı (ı' T) == T.
   Proof. apply (UF_id T). Qed.
 
+  Set Printing All.
+  (* 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.