Merge PR #11820: Partial imports

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

4 files changed, 69 insertions, 6 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 78b1f02383..57c8683aaa 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -422,7 +422,12 @@ are now available through the dot notation.
    If :n:`@module_binder`\s are specified, declares a functor with parameters given by the list of
    :token:`module_binder`\s.
 
-.. cmd:: Import {+ @qualid }
+.. cmd:: Import {+ @filtered_import }
+
+   .. insertprodn filtered_import filtered_import
+
+   .. prodn::
+      filtered_import ::= @qualid {? ( {+, @qualid {? ( .. ) } } ) }
 
    If :token:`qualid` denotes a valid basic module (i.e. its module type is a
    signature), makes its components available by their short names.
@@ -465,12 +470,50 @@ are now available through the dot notation.
 
          Check B.T.
 
-.. cmd:: Export {+ @qualid }
+   Appending a module name with a parenthesized list of names will
+   make only those names available with short names, not other names
+   defined in the module nor will it activate other features.
+
+   The names to import may be constants, inductive types and
+   constructors, and notation aliases (for instance, Ltac definitions
+   cannot be selectively imported). If they are from an inner module
+   to the one being imported, they must be prefixed by the inner path.
+
+   The name of an inductive type may also be followed by ``(..)`` to
+   import it, its constructors and its eliminators if they exist. For
+   this purpose "eliminator" means a constant in the same module whose
+   name is the inductive type's name suffixed by one of ``_sind``,
+   ``_ind``, ``_rec`` or ``_rect``.
+
+   .. example::
+
+      .. coqtop:: reset in
+
+         Module A.
+         Module B.
+         Inductive T := C.
+         Definition U := nat.
+         End B.
+         Definition Z := Prop.
+         End A.
+         Import A(B.T(..), Z).
+
+      .. coqtop:: all
+
+         Check B.T.
+         Check B.C.
+         Check Z.
+         Fail Check B.U.
+         Check A.B.U.
+
+.. cmd:: Export {+ @filtered_import }
    :name: Export
 
    Similar to :cmd:`Import`, except that when the module containing this command
    is imported, the :n:`{+ @qualid }` are imported as well.
 
+   The selective import syntax also works with Export.
+
    .. exn:: @qualid is not a module.
       :undocumented:
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a01f57eb22..5034d9a3c9 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -511,6 +511,12 @@ strategy_flag: [
 | OPTINREF
 ]
 
+filtered_import: [
+| REPLACE global "(" LIST1 one_import_filter_name SEP "," ")"
+| WITH global OPT [ "(" LIST1 one_import_filter_name SEP "," ")" ]
+| DELETE global
+]
+
 functor_app_annot: [
 | OPTINREF
 ]
@@ -1582,6 +1588,7 @@ SPLICE: [
 | searchabout_queries
 | locatable
 | scope_delimiter
+| one_import_filter_name
 ] (* end SPLICE *)
 
 RENAME: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index dc7e0fba37..04c20a7203 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1031,8 +1031,8 @@ gallina_ext: [
 | "Collection" identref ":=" section_subset_expr
 | "Require" export_token LIST1 global
 | "From" global "Require" export_token LIST1 global
-| "Import" LIST1 global
-| "Export" LIST1 global
+| "Import" LIST1 filtered_import
+| "Export" LIST1 filtered_import
 | "Include" module_type_inl LIST0 ext_module_expr
 | "Include" "Type" module_type_inl LIST0 ext_module_type
 | "Transparent" LIST1 smart_global
@@ -1057,6 +1057,15 @@ gallina_ext: [
 | "Export" "Unset" option_table
 ]
 
+filtered_import: [
+| global
+| global "(" LIST1 one_import_filter_name SEP "," ")"
+]
+
+one_import_filter_name: [
+| global OPT [ "(" ".." ")" ]
+]
+
 export_token: [
 | "Import"
 | "Export"
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index ac986f9adf..e71c80f829 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -497,6 +497,10 @@ constructor: [
 | ident LIST0 binder OPT of_type
 ]
 
+filtered_import: [
+| qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ]
+]
+
 cofix_definition: [
 | ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations
 ]
@@ -849,8 +853,8 @@ command: [
 | "Collection" ident ":=" section_subset_expr
 | "Require" OPT [ "Import" | "Export" ] LIST1 qualid
 | "From" dirpath "Require" OPT [ "Import" | "Export" ] LIST1 qualid
-| "Import" LIST1 qualid
-| "Export" LIST1 qualid
+| "Import" LIST1 filtered_import
+| "Export" LIST1 filtered_import
 | "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
 | "Include" "Type" LIST1 module_type_inl SEP "<+"
 | "Transparent" LIST1 smart_qualid