code cleaning + deals better with the new module system of Coq. Did

not test the fsfemacs. Will do before release.

1 files changed, 41 insertions, 22 deletions

diff --git a/coq/ex-module.v b/coq/ex-module.v
index e9d42072..f8df0c31 100644
--- a/coq/ex-module.v
+++ b/coq/ex-module.v
@@ -4,46 +4,65 @@ Module M.
     Parameter T:Set.
     Parameter x:T.
   End SIG.
+  Lemma toto : O=O.
+  Definition t:=nat.
+	 Trivial.
+  Save.
   Module N:SIG.
     Definition T:=nat.
     Definition x:=O.
   End N.
+  Module O:=N.
 End M.
 
+Definition t:O=O.
+Trivial.
+Save.
+
+
 Section toto.
 Print M.
 End toto.
 
+  Module N:=M.
 
-Lemma toto : O=O.
-Module N:=M.
-Definition t:=M.N.T.
-Trivial.
-Save.
+Module R:N.SIG.
+ Definition T:Set:=nat.
+ Definition x:T:= O.
+ Definition foo:nat:=(S O).
+End R.
 
 
-Module Type SPRYT.
-  Module N.
-    Definition T:=M.N.T.
-    Parameter x:T.
-  End N.
-End SPRYT.
+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 *)
+End N'.
+
 
-Module K:SPRYT:=N.  
-Module K':SPRYT:=M.  
 
 Lemma titi : O=O.
-Module Type S:=SPRYT.
-Module N':=M.
 Trivial.
+Module Type K:=N'.
+Module N''':=M.
 Save.
 
+(* Here is a bug of Coq: *)
 
-Module Type SIG.
-  Definition T:Set:=M.N.T.
-  Parameter x:T.
-
-  Module N:SPRYT.
-End SIG.
+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.
 
-Module J:M.SIG:=M.N.