From a2686239fa742bc761f003608f276a82a4c5cae7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 24 Feb 2020 15:31:44 +0100
Subject: test partial import

---
 test-suite/success/PartialImport.v | 45 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 test-suite/success/PartialImport.v

diff --git a/test-suite/success/PartialImport.v b/test-suite/success/PartialImport.v
new file mode 100644
index 0000000000..8306d79352
--- /dev/null
+++ b/test-suite/success/PartialImport.v
@@ -0,0 +1,45 @@
+Module M.
+
+  Definition a := 0.
+  Definition b := 1.
+
+  Module N.
+
+    Notation c := (a + b).
+
+  End N.
+
+End M.
+
+Module Simple.
+
+  Import M(a).
+
+  Check a.
+  Fail Check b.
+  Fail Check N.c.
+
+  (* todo output test: this prints a+M.b since the notation isn't imported *)
+  Check M.N.c.
+
+  Fail Import M(c).
+  Fail Import M(M.b).
+
+  Import M(N.c).
+  Check N.c.
+  (* interestingly prints N.c (also does with unfiltered Import M) *)
+
+End Simple.
+
+Module WithExport.
+
+  Module X.
+    Export M(a, N.c).
+  End X.
+
+  Import X.
+  Check a.
+  Check N.c. (* also prints N.c *)
+  Fail Check b.
+
+End WithExport.
-- 
cgit v1.2.3