1 files changed, 75 insertions, 0 deletions
diff --git a/test-suite/success/import_mod.v b/test-suite/success/import_mod.v
new file mode 100644
index 00000000..b4a8af46
--- /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.