Partial import inductive(..)

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

7 files changed, 54 insertions, 5 deletions

diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 466fbacca4..3a89b73bd5 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -12,6 +12,8 @@ open Univ
 
 type family = InSProp | InProp | InSet | InType
 
+let all_families = [InSProp; InProp; InSet; InType]
+
 type t =
   | SProp
   | Prop
diff --git a/kernel/sorts.mli b/kernel/sorts.mli
index 49549e224d..fe939b1d95 100644
--- a/kernel/sorts.mli
+++ b/kernel/sorts.mli
@@ -12,6 +12,8 @@
 
 type family = InSProp | InProp | InSet | InType
 
+val all_families : family list
+
 type t = private
   | SProp
   | Prop
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.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 642f504050..08ba49f92b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -576,7 +576,10 @@ GRAMMAR EXTEND Gram
   ;
   filtered_import:
     [ [ m = global -> { (m, ImportAll) }
-      | m = global; "("; ns = LIST1 global SEP ","; ")" -> { (m, ImportNames ns) } ] ]
+      | m = global; "("; ns = LIST1 one_import_filter_name SEP ","; ")" -> { (m, ImportNames ns) } ] ]
+  ;
+  one_import_filter_name:
+    [ [ n = global; etc = OPT [ "("; ".."; ")" -> { () } ] -> { n, Option.has_some etc } ] ]
   ;
   export_token:
     [ [ IDENT "Import" -> { Some false }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index be57fc37e7..baaf8aa849 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -86,10 +86,13 @@ open Pputils
 
   let pr_module = Libnames.pr_qualid
 
+  let pr_one_import_filter_name (q,etc) =
+    Libnames.pr_qualid q ++ if etc then str "(..)" else mt()
+
   let pr_import_module (m,f) =
     Libnames.pr_qualid m ++ match f with
     | ImportAll -> mt()
-    | ImportNames ns -> surround (prlist_with_sep pr_comma Libnames.pr_qualid ns)
+    | ImportNames ns -> surround (prlist_with_sep pr_comma pr_one_import_filter_name ns)
 
   let sep_end = function
     | VernacBullet _
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index cf7b43bde0..6de14997d4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -872,13 +872,37 @@ let vernac_constraint ~poly l =
 (**********************)
 (* Modules            *)
 
+let add_subnames_of ns full_n n =
+  let open GlobRef in
+  let module NSet = Globnames.ExtRefSet in
+  let add1 r ns = NSet.add (Globnames.TrueGlobal r) ns in
+  match n with
+  | Globnames.SynDef _ | Globnames.TrueGlobal (ConstRef _ | ConstructRef _ | VarRef _) ->
+    CErrors.user_err Pp.(str "Only inductive types can be used with Import (...).")
+  | Globnames.TrueGlobal (IndRef (mind,i)) ->
+    let open Declarations in
+    let dp = Libnames.dirpath full_n in
+    let mib = Global.lookup_mind mind in
+    let mip = mib.mind_packets.(i) in
+    let ns = add1 (IndRef (mind,i)) ns in
+    let ns = Array.fold_left_i (fun j ns _ -> add1 (ConstructRef ((mind,i),j+1)) ns)
+        ns mip.mind_consnames
+    in
+    List.fold_left (fun ns f ->
+        let s = Indrec.elimination_suffix f in
+        let n_elim = Id.of_string (Id.to_string mip.mind_typename ^ s) in
+        match Nametab.extended_global_of_path (Libnames.make_path dp n_elim) with
+        | exception Not_found -> ns
+        | n_elim -> NSet.add n_elim ns)
+      ns Sorts.all_families
+
 let interp_filter_in m = function
   | ImportAll ->  Libobject.Unfiltered
   | ImportNames ns ->
     let module NSet = Globnames.ExtRefSet in
     let dp_m = Nametab.dirpath_of_module m in
     let ns =
-      List.fold_left (fun ns n ->
+      List.fold_left (fun ns (n,etc) ->
           let full_n =
             let dp_n,n = repr_qualid n in
             make_path (append_dirpath dp_m dp_n) n
@@ -889,7 +913,8 @@ let interp_filter_in m = function
                 Pp.(str "Cannot find name " ++ pr_qualid n ++ spc() ++
                     str "in module " ++ pr_qualid (Nametab.shortest_qualid_of_module m))
           in
-          NSet.add n ns)
+          let ns = NSet.add n ns in
+          if etc then add_subnames_of ns full_n n else ns)
         NSet.empty ns
     in
     Libobject.Names ns
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 70ccfc139d..27663a0681 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -104,9 +104,10 @@ type instance_flag  = bool option
 
 type export_flag    = bool (* true = Export;        false = Import         *)
 
+type one_import_filter_name = qualid * bool (* import inductive components *)
 type import_filter_expr =
   | ImportAll
-  | ImportNames of qualid list
+  | ImportNames of one_import_filter_name list
 
 type onlyparsing_flag = { onlyparsing : bool }
  (* Some v = Parse only;  None = Print also.