diff options
| author | Théo Zimmermann | 2020-03-27 16:48:22 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 15:18:18 +0200 |
| commit | 4ca67150e972899bc84e78c589833ba06a66aa21 (patch) | |
| tree | 46253957ab62b212e882362704b1c84d705236c9 /doc/tools/docgram/fullGrammar | |
| parent | ff99fb50b26ea4065daa8ae5b1c98ad5e6ba659a (diff) | |
Update syntax of Import / Export in documentation.
Diffstat (limited to 'doc/tools/docgram/fullGrammar')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 13 |
1 files changed, 11 insertions, 2 deletions
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" |