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 /vernac | |
| 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 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 31fc54c1fa..1f52641b82 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -199,8 +199,8 @@ GRAMMAR EXTEND Gram VernacAssumption (stre, nl, bl) } | d = def_token; id = ident_decl; b = def_body -> { VernacDefinition (d, name_of_ident_decl id, b) } - | IDENT "Let"; id = identref; b = def_body -> - { VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) } + | IDENT "Let"; id = ident_decl; b = def_body -> + { VernacDefinition ((DoDischarge, Let), name_of_ident_decl id, b) } (* Gallina inductive declarations *) | f = finite_token; indl = LIST1 inductive_definition SEP "with" -> { VernacInductive (f, indl) } |