indentation for coq completely re-coded, because the generic mechanism

does not use "proof-goal-command-p" and is not powerful enough.

1 files changed, 33 insertions, 33 deletions

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.