From ca05bbc391f48d5e56e24a653c6a7799909eed4d Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <courtieu@lri.fr>
Date: Mon, 8 Mar 2004 18:41:59 +0000
Subject: indentation for coq completely re-coded, because the generic
 mechanism does not use "proof-goal-command-p" and is not powerful enough.

---
 coq/ex-module.v | 66 ++++++++++++++++++++++++++++-----------------------------
 1 file changed, 33 insertions(+), 33 deletions(-)

(limited to 'coq/ex-module.v')

diff --git a/coq/ex-module.v b/coq/ex-module.v
index 227b3ff7..2fbdbcf5 100644
--- a/coq/ex-module.v
+++ b/coq/ex-module.v
@@ -1,22 +1,22 @@
 
 Module Type O1.
-Parameter A:Set.
-Parameter B:Set.
+  Parameter A:Set.
+  Parameter B:Set.
 End O1.
 
 
 Module R:O1.
-Definition A:=nat.
-Definition B:=bool.
+  Definition A:=nat.
+  Definition B:=bool.
 End R.
 
 Module R2: O1 with Definition  A:=nat.
-Definition A:=nat.
-Definition B:=bool.
+  Definition A:=nat.
+  Definition B:=bool.
 End R2.
 
 Module R4.
-Module R3: O1 with Definition  A:=nat :=R2.
+  Module R3: O1 with Definition  A:=nat :=R2.
 End R4.
 
 
@@ -28,8 +28,8 @@ Module M.
     Parameter x:T.
   End SIG.
   Lemma toto : O=O.
-  Definition t:=nat.
-	 Trivial.
+    Definition t:=nat.
+    Trivial.
   Save.
   Module N:SIG.
     Definition T:=nat.
@@ -43,54 +43,54 @@ Print t.
 
 
 Definition t:O=O.
-Trivial.
+  Trivial.
 Save.
 
 
 Section toto.
-Print M.
+  Print M.
 End toto.
 
 Module N:=M.
 
 
 Module Type typ.
-Parameter T:Set.
-Parameter a:T.
+  Parameter T:Set.
+  Parameter a:T.
 End typ.
 
 
 
 Module Type N'.
-Module Type M'.
-Declare Module K:N.SIG.
-End M'.
-Declare Module 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 *)
+  Module Type M'.
+    Declare Module K:N.SIG.
+  End M'.
+  Declare Module 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.
+  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.
+  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.
 
-- 
cgit v1.2.3