diff options
| author | Théo Zimmermann | 2020-02-06 13:29:35 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-07 17:37:03 +0200 |
| commit | 2e8e25217abe62ebf0ed17c3ef6c48f595699433 (patch) | |
| tree | 60165c4e23af88352ab117f236d4d11b75383bac /doc/tools/docgram/orderedGrammar | |
| parent | 2089207415565e8a28816f53b61d9292d04f4c59 (diff) | |
Support universe bindings and universe constraints in Let definitions.
Let vs Definition / Example syntax was split in 7c28130 for parsing
reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could
be introduced. This split is probably the reason why Let was
overlooked when support for universe bindings and universe constraints
were added to Definition and variants.
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 |