diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -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) } |