4 files changed, 46 insertions, 27 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index b448d0f9d3..57243207f0 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -188,20 +188,19 @@ class CoqObject(ObjectDescription):
     def _add_index_entry(self, name, target):
         """Add `name` (pointing to `target`) to the main index."""
         assert isinstance(name, str)
-        if not name.startswith("_"):
-            # remove trailing . , found in commands, but not ... (ellipsis)
-            trim = name.endswith(".") and not name.endswith("...")
-            index_text = name[:-1] if trim else name
-            if self.index_suffix:
-                index_text += " " + self.index_suffix
-            self.indexnode['entries'].append(('single', index_text, target, '', None))
+        # remove trailing . , found in commands, but not ... (ellipsis)
+        trim = name.endswith(".") and not name.endswith("...")
+        index_text = name[:-1] if trim else name
+        if self.index_suffix:
+            index_text += " " + self.index_suffix
+        self.indexnode['entries'].append(('single', index_text, target, '', None))
 
     aliases = None  # additional indexed names for a command or other object
 
     def add_target_and_index(self, name, _, signode):
         """Attach a link target to `signode` and an index entry for `name`.
         This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified."""
-        if name:
+        if name and not (isinstance(name, str) and name.startswith('_')):
             target = self._add_target(signode, name)
             self._add_index_entry(name, target)
             if self.aliases is not None:
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a01f57eb22..700170b3c6 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
 ]
@@ -900,14 +906,14 @@ command: [
 | DELETE "Unset" option_table
 | REPLACE "Set" option_table option_setting
 | WITH OPT "Export" "Set" option_table   (* set flag *)
-| REPLACE "Test" option_table "for" LIST1 option_ref_value
-| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value )
+| REPLACE "Test" option_table "for" LIST1 table_value
+| WITH "Test" option_table OPT ( "for" LIST1 table_value )
 | DELETE "Test" option_table
 
 (* hide the fact that table names are limited to 2 IDENTs *)
-| REPLACE "Add" IDENT IDENT LIST1 option_ref_value
-| WITH "Add" option_table LIST1 option_ref_value
-| DELETE "Add" IDENT LIST1 option_ref_value
+| REPLACE "Add" IDENT IDENT LIST1 table_value
+| WITH "Add" option_table LIST1 table_value
+| DELETE "Add" IDENT LIST1 table_value
 | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
 | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident
 | DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
@@ -963,9 +969,9 @@ command: [
 | DELETE "Preterm"
 
 (* hide the fact that table names are limited to 2 IDENTs *)
-| REPLACE "Remove" IDENT IDENT LIST1 option_ref_value
-| WITH "Remove" option_table LIST1 option_ref_value
-| DELETE "Remove" IDENT LIST1 option_ref_value
+| REPLACE "Remove" IDENT IDENT LIST1 table_value
+| WITH "Remove" option_table LIST1 table_value
+| DELETE "Remove" IDENT LIST1 table_value
 | DELETE "Restore" "State" IDENT
 | DELETE "Restore" "State" ne_string
 | "Restore" "State" [ IDENT | ne_string ]
@@ -1544,7 +1550,7 @@ SPLICE: [
 | constructor_type
 | record_binder
 | at_level_opt
-| option_ref_value
+| table_value
 | positive_search_mark
 | in_or_out_modules
 | option_setting
@@ -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..4274dccb40 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -524,12 +524,12 @@ command: [
 | "Set" option_table option_setting
 | "Unset" option_table
 | "Print" "Table" option_table
-| "Add" IDENT IDENT LIST1 option_ref_value
-| "Add" IDENT LIST1 option_ref_value
-| "Test" option_table "for" LIST1 option_ref_value
+| "Add" IDENT IDENT LIST1 table_value
+| "Add" IDENT LIST1 table_value
+| "Test" option_table "for" LIST1 table_value
 | "Test" option_table
-| "Remove" IDENT IDENT LIST1 option_ref_value
-| "Remove" IDENT LIST1 option_ref_value
+| "Remove" IDENT IDENT LIST1 table_value
+| "Remove" IDENT LIST1 table_value
 | "Write" "State" IDENT
 | "Write" "State" ne_string
 | "Restore" "State" IDENT
@@ -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"
@@ -1309,7 +1318,7 @@ option_setting: [
 | STRING
 ]
 
-option_ref_value: [
+table_value: [
 | global
 | STRING
 ]
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