Merge PR #11820: Partial imports

Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot

3 files changed, 70 insertions, 0 deletions

diff --git a/test-suite/output/UselessSyndef.out b/test-suite/output/UselessSyndef.out
new file mode 100644
index 0000000000..ce484889b3
--- /dev/null
+++ b/test-suite/output/UselessSyndef.out
@@ -0,0 +1,2 @@
+a
+     : nat
diff --git a/test-suite/output/UselessSyndef.v b/test-suite/output/UselessSyndef.v
new file mode 100644
index 0000000000..96ad6e9f5c
--- /dev/null
+++ b/test-suite/output/UselessSyndef.v
@@ -0,0 +1,10 @@
+Module M.
+  Definition a := 0.
+End M.
+Module N.
+  Notation a := M.a (only parsing).
+End N.
+
+Import M. Import N.
+
+Check a.
diff --git a/test-suite/success/PartialImport.v b/test-suite/success/PartialImport.v
new file mode 100644
index 0000000000..720083aec5
--- /dev/null
+++ b/test-suite/success/PartialImport.v
@@ -0,0 +1,58 @@
+Module M.
+
+  Definition a := 0.
+  Definition b := 1.
+
+  Module N.
+
+    Notation c := (a + b).
+
+  End N.
+
+  Inductive even : nat -> Prop :=
+  | even_0 : even 0
+  | even_S n : odd n -> even (S n)
+  with odd : nat -> Set :=
+    odd_S n : even n -> odd (S 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) *)
+
+  Import M(even(..)).
+  Check even. Check even_0. Check even_S.
+  Check even_sind. Check even_ind.
+  Fail Check even_rect. (* doesn't exist *)
+  Fail Check odd. Check M.odd.
+  Fail Check odd_S. Fail Check odd_sind.
+
+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.