From 1113f98eec9b488e1ce5a852f1daffec0a25f2c9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 9 Feb 2015 17:17:57 +0100
Subject: [PATCH] coq formatting

---
 world_prop.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/world_prop.v b/world_prop.v
index 6108c4c89..be2fd5e60 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.
 
-- 
GitLab