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/sphinx/language/gallina-extensions.rst | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx/language')

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index cbdfdab1ca..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.
@@ -501,7 +506,7 @@ are now available through the dot notation.
          Fail Check B.U.
          Check A.B.U.
 
-.. cmd:: Export {+ @qualid }
+.. cmd:: Export {+ @filtered_import }
    :name: Export
 
    Similar to :cmd:`Import`, except that when the module containing this command
-- 
cgit v1.2.3