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/docgram/orderedGrammar | |
| 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/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 3 |
1 files changed, 1 insertions, 2 deletions
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 |