3 files changed, 39 insertions, 19 deletions
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