diff --git a/world_prop.v b/world_prop.v
index 6108c4c892bcd29ca1884e73d2d6cf1dd05b6cc7..be2fd5e60f23e06ba605ab6b9c6f161570eb30e4 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -7,11 +7,11 @@ Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI.
 
 (* This interface keeps some of the details of the solution opaque *)
 Module Type WORLD_PROP (Res : PCM_T).
-  (* PreProp: The solution to the recursive equation. Equipped with a discrete order *)
+  (* PreProp: The solution to the recursive equation. Equipped with a discrete order. *)
   Parameter PreProp    : cmtyp.
-  Instance PProp_preo: preoType PreProp   := disc_preo PreProp.
-  Instance PProp_pcm : pcmType PreProp    := disc_pcm PreProp.
-  Instance PProp_ext : extensible PreProp := disc_ext 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.
 
   (* Defines Worlds, Propositions *)
   Definition Wld       := nat -f> PreProp.
@@ -24,7 +24,6 @@ Module Type WORLD_PROP (Res : PCM_T).
   Instance Props_preo : preoType Props| 1 := _.
   Instance Props_pcm  : pcmType Props | 1 := _.
 
-  
   (* Establish the recursion isomorphism *)
   Parameter ı  : PreProp -n> halve (cmfromType Props).
   Parameter ı' : halve (cmfromType Props) -n> PreProp.
@@ -32,6 +31,7 @@ Module Type WORLD_PROP (Res : PCM_T).
   Axiom isoR: forall T, ı (ı' T) == T.
 End WORLD_PROP.
 
+
 (* Now we come to the actual implementation *)
 Module WorldProp (Res : PCM_T) : WORLD_PROP Res.