Correction du bug 335 et Export/Require Export dans un module

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 280 insertions, 0 deletions

diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index f94ed64234..41e8648bc0 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,7 +1,10 @@
 TrM.A = M.A
      : Set
+
 OpM.A = M.A
      : Set
+
 TrM.B = M.B
      : Set
+
 *** [ OpM.B : Set ]
diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v
new file mode 100644
index 0000000000..b354362472
--- /dev/null
+++ b/test-suite/success/import_lib.v
@@ -0,0 +1,202 @@
+Definition le_trans:=O.
+
+
+Module Test_Read.     
+  Module M.  
+    Read Module Le.        (* Reading without importing *)
+
+    Check Le.le_trans.
+
+    Lemma th0 : le_trans = O.
+      Reflexivity.
+    Qed.
+  End M.
+
+  Check Le.le_trans. 
+
+  Lemma th0 : le_trans = O.
+    Reflexivity.
+  Qed.
+
+  Import M.
+
+  Lemma th1 : le_trans = O.
+    Reflexivity.
+  Qed.
+End Test_Read.
+
+
+(****************************************************************)
+
+Definition le_decide := (S O).  (* from Arith/Compare *)
+Definition min := O.            (* from Arith/Min *)
+
+Module Test_Require.
+  
+  Module M.
+    Require Compare.              (* Imports Min as well *)
+  
+    Lemma th1 : le_decide = Compare.le_decide.
+      Reflexivity.
+    Qed.
+  
+    Lemma th2 : min = Min.min.
+      Reflexivity.
+    Qed.
+  
+  End M.
+  
+  (* Checks that Compare and List are loaded *)
+  Check Compare.le_decide.
+  Check Min.min.
+  
+  
+  (* Checks that Compare and List are _not_ imported *)
+  Lemma th1 : le_decide = (S O).
+    Reflexivity.
+  Qed.
+  
+  Lemma th2 : min = O.
+    Reflexivity.
+  Qed.
+  
+  (* It should still be the case after Import M *)
+  Import M.
+  
+  Lemma th3 : le_decide = (S O).
+    Reflexivity.
+  Qed.
+  
+  Lemma th4 : min = O.
+    Reflexivity.
+  Qed.
+
+End Test_Require.  
+
+(****************************************************************)
+
+Module Test_Import.
+  Module M.
+    Import Compare.              (* Imports Min as well *)
+  
+    Lemma th1 : le_decide = Compare.le_decide.
+      Reflexivity.
+    Qed.
+  
+    Lemma th2 : min = Min.min.
+      Reflexivity.
+    Qed.
+  
+  End M.
+  
+  (* Checks that Compare and List are loaded *)
+  Check Compare.le_decide.
+  Check Min.min.
+  
+  
+  (* Checks that Compare and List are _not_ imported *)
+  Lemma th1 : le_decide = (S O).
+    Reflexivity.
+  Qed.
+  
+  Lemma th2 : min = O.
+    Reflexivity.
+  Qed.
+  
+  (* It should still be the case after Import M *)
+  Import M.
+  
+  Lemma th3 : le_decide = (S O).
+    Reflexivity.
+  Qed.
+  
+  Lemma th4 : min = O.
+    Reflexivity.
+  Qed.
+End Test_Import.
+
+(***********************************************************************)
+
+Module Test_Export.
+  Module M.
+    Export Compare.              (* Exports Min as well *)
+
+    Lemma th1 : le_decide = Compare.le_decide.
+      Reflexivity.
+    Qed.
+
+    Lemma th2 : min = Min.min.
+      Reflexivity.
+    Qed.
+
+  End M.
+
+
+  (* Checks that Compare and List are _not_ imported *)
+  Lemma th1 : le_decide = (S O).
+    Reflexivity.
+  Qed.
+
+  Lemma th2 : min = O.
+    Reflexivity.
+  Qed.
+
+
+  (* After Import M they should be imported as well *)
+
+  Import M.
+
+  Lemma th3 : le_decide = Compare.le_decide.
+    Reflexivity.
+  Qed.
+
+  Lemma th4 : min = Min.min.
+    Reflexivity.
+  Qed.
+End Test_Export.
+
+
+(***********************************************************************)
+
+Module Test_Require_Export.
+
+  Definition mult_sym:=(S O).    (* from Arith/Mult *)
+  Definition plus_sym:=O.        (* from Arith/Plus *)
+
+  Module M.
+    Require Export Mult.         (* Exports Plus as well *)
+
+    Lemma th1 : mult_sym = Mult.mult_sym.
+      Reflexivity.
+    Qed.
+
+    Lemma th2 : plus_sym = Plus.plus_sym.
+      Reflexivity.
+    Qed.
+
+  End M.
+
+
+  (* Checks that Mult and Plus are _not_ imported *)
+  Lemma th1 : mult_sym = (S O).
+    Reflexivity.
+  Qed.
+
+  Lemma th2 : plus_sym = O.
+    Reflexivity.
+  Qed.
+
+
+  (* After Import M they should be imported as well *)
+
+  Import M.
+
+  Lemma th3 : mult_sym = Mult.mult_sym.
+    Reflexivity.
+  Qed.
+
+  Lemma th4 : plus_sym = Plus.plus_sym.
+    Reflexivity.
+  Qed.
+
+End Test_Require_Export.
diff --git a/test-suite/success/import_mod.v b/test-suite/success/import_mod.v
new file mode 100644
index 0000000000..b4a8af46fd
--- /dev/null
+++ b/test-suite/success/import_mod.v
@@ -0,0 +1,75 @@
+
+Definition p:=O.
+Definition m:=O.
+
+Module Test_Import.
+  Module P.
+    Definition p:=(S O).
+  End P.
+
+  Module M.
+    Import P.
+    Definition m:=p.
+  End M.
+
+  Module N.
+    Import M.
+
+    Lemma th0 : p=O.
+      Reflexivity.
+    Qed.
+
+  End N.
+
+
+  (* M and P should be closed *)
+  Lemma th1 : m=O /\ p=O.
+    Split; Reflexivity.
+  Qed.
+
+
+  Import N.
+
+  (* M and P should still be closed *)
+  Lemma th2 : m=O /\ p=O.
+    Split; Reflexivity.
+  Qed.
+End Test_Import.
+
+
+(********************************************************************)
+
+
+Module Test_Export.
+  Module P.
+    Definition p:=(S O).
+  End P.
+
+  Module M.
+    Export P.
+    Definition m:=p.
+  End M.
+
+  Module N.
+    Export M.
+
+    Lemma th0 : p=(S O).
+      Reflexivity.
+    Qed.
+
+  End N.
+
+
+  (* M and P should be closed *)
+  Lemma th1 : m=O /\ p=O.
+    Split; Reflexivity.
+  Qed.
+
+
+  Import N.
+
+  (* M and P should now be opened *)
+  Lemma th2 : m=(S O) /\ p=(S O).
+    Split; Reflexivity.
+  Qed.
+End Test_Export.