Use official indentation\!

2 files changed, 32 insertions, 31 deletions

diff --git a/coq/ex-module.v b/coq/ex-module.v
index 2fbdbcf5..af2e4a08 100644
--- a/coq/ex-module.v
+++ b/coq/ex-module.v
@@ -10,7 +10,8 @@ Module R:O1.
   Definition B:=bool.
 End R.
 
-Module R2: O1 with Definition  A:=nat.
+Module R2: O1 with 
+  Definition  A:=nat.
   Definition A:=nat.
   Definition B:=bool.
 End R2.
@@ -69,28 +70,28 @@ Module Type N'.
     Definition T:=nat.
     Definition x:=O.
   End N''.
-
+  
   Declare Module N':M.SIG. (* no interactive def started *)
-  Declare Module N''':= N'. (* no interactive def started *)
-  Declare Module N''''. (* interactive def started *)
-    Parameter foo:nat.
-  End N''''.            (* interactive def ended *)
-End N'.
-
-
-
-Lemma titi : O=O.
-  Trivial.
-  Module Type K:=N'.
-  Module N''':=M.
-Save.
-
-(* Here is a bug of Coq: *)
-
-Lemma bar:O=O.
-  Module Type L. (* This should not be allowed by Coq, since the End L. below fails *)
-    Axiom foo: O=O.
-  End L. (* fails --> if we go back to Module Type: unsync *)
-  Module I.
-End I.
-
+    Declare Module N''':= N'. (* no interactive def started *)
+      Declare Module N''''. (* interactive def started *)
+	Parameter foo:nat.
+      End N''''.            (* interactive def ended *)
+    End N'.
+
+    
+    
+    Lemma titi : O=O.
+      Trivial.
+      Module Type K:=N'.
+      Module N''':=M.
+    Save.
+
+  (* Here is a bug of Coq: *)
+    
+    Lemma bar:O=O.
+      Module Type L. (* This should not be allowed by Coq, since the End L. below fails *)
+	Axiom foo: O=O.
+      End L. (* fails --> if we go back to Module Type: unsync *)
+      Module I.
+    End I.
+    
diff --git a/coq/example.v b/coq/example.v
index d9976ea7..cfe85203 100644
--- a/coq/example.v
+++ b/coq/example.v
@@ -5,10 +5,10 @@
 *)
 
 Goal (A,B:Prop)(A /\ B) -> (B /\ A).
- Intros A B H.
- Elim H.
- Intros.
- Split.
- Assumption.
- Assumption.
+  Intros A B H.
+  Elim H.
+  Intros.
+  Split.
+  Assumption.
+  Assumption.
 Save and_comms.