Partial import inductive(..)

NB: 3 dots doesn't play well with PG's sentence detection.

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/success/PartialImport.v b/test-suite/success/PartialImport.v
index 8306d79352..720083aec5 100644
--- a/test-suite/success/PartialImport.v
+++ b/test-suite/success/PartialImport.v
@@ -9,6 +9,12 @@ Module M.
 
   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.
@@ -29,6 +35,13 @@ Module Simple.
   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.