diff options
| author | Gaëtan Gilbert | 2020-04-09 13:21:00 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-09 13:21:00 +0200 |
| commit | 75589e466c9f0ed62dd10fff6c1f7d284c7ffa89 (patch) | |
| tree | de1aca49cec2cc8dd4c71f26d53e0ade8490965b /doc/tools | |
| parent | 13e727ae9c7400ae0f2d9c2a5057c50e1d9b5858 (diff) | |
| parent | 2e8e25217abe62ebf0ed17c3ef6c48f595699433 (diff) | |
Merge PR #11534: Support universe bindings and universe constraints in Let definitions.
Reviewed-by: SkySkimmer
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 3 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 3 |
2 files changed, 2 insertions, 4 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 272d17bb35..dc7e0fba37 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -773,7 +773,7 @@ gallina: [ | assumption_token inline assum_list | assumptions_token inline assum_list | def_token ident_decl def_body -| "Let" identref def_body +| "Let" ident_decl def_body | finite_token LIST1 inductive_definition SEP "with" | "Fixpoint" LIST1 rec_definition SEP "with" | "Let" "Fixpoint" LIST1 rec_definition SEP "with" @@ -1027,7 +1027,6 @@ gallina_ext: [ | "Module" "Type" identref LIST0 module_binder check_module_types is_module_type | "Declare" "Module" export_token identref LIST0 module_binder ":" module_type_inl | "Section" identref -| "Chapter" identref | "End" identref | "Collection" identref ":=" section_subset_expr | "Require" export_token LIST1 global diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 0c9d7a853b..535976b7d9 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -851,7 +851,7 @@ command: [ | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] | assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] | [ "Definition" | "Example" ] ident_decl def_body -| "Let" ident def_body +| "Let" ident_decl def_body | "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) | "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) | "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) @@ -873,7 +873,6 @@ command: [ | "Module" "Type" ident LIST0 module_binder LIST0 ( "<:" module_type_inl ) OPT ( ":=" LIST1 module_type_inl SEP "<+" ) | "Declare" "Module" OPT [ "Import" | "Export" ] ident LIST0 module_binder ":" module_type_inl | "Section" ident -| "Chapter" ident | "End" ident | "Collection" ident ":=" section_subset_expr | "Require" OPT [ "Import" | "Export" ] LIST1 qualid |