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 /vernac | |
| parent | 13e727ae9c7400ae0f2d9c2a5057c50e1d9b5858 (diff) | |
| parent | 2e8e25217abe62ebf0ed17c3ef6c48f595699433 (diff) | |
Merge PR #11534: Support universe bindings and universe constraints in Let definitions.
Reviewed-by: SkySkimmer
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) } |