From 4ca67150e972899bc84e78c589833ba06a66aa21 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 27 Mar 2020 16:48:22 +0100
Subject: Update syntax of Import / Export in documentation.

---
 doc/tools/docgram/orderedGrammar | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'doc/tools/docgram/orderedGrammar')

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
-- 
cgit v1.2.3