diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_proofs.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index e84fce5504..f2a1dce01d 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -98,7 +98,7 @@ GRAMMAR EXTEND Gram | IDENT "Guarded" -> { VernacCheckGuard } (* Hints for Auto and EAuto *) | IDENT "Create"; IDENT "HintDb" ; - id = IDENT ; b = [ "discriminated" -> { true } | -> { false } ] -> + id = IDENT ; b = [ IDENT "discriminated" -> { true } | -> { false } ] -> { VernacCreateHintDb (id, b) } | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> { VernacRemoveHints (dbnames, ids) } |