diff options
| author | Théo Zimmermann | 2020-05-13 13:06:08 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-13 13:06:08 +0200 |
| commit | d80458841316ca7edf7317ef412142e27133c931 (patch) | |
| tree | 3baabb2bcd428af714fc0bcb2183f42e14c9efff /vernac | |
| parent | 23be910b49eac7a69a30b1e737a4738e24edcaa0 (diff) | |
| parent | 037c8d299ca1a5aef9813133dca07ad6f35e1e75 (diff) | |
Merge PR #12229: Hopefully consensual cleaning of keywords
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_proofs.mlg | 2 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 3 |
2 files changed, 1 insertions, 4 deletions
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 058fa691ee..80a4de472c 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -97,7 +97,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) } diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 049c3a0844..42259cee10 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -30,9 +30,6 @@ open Pcoq.Module open Pvernac.Vernac_ open Attributes -let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] -let _ = List.iter CLexer.add_keyword vernac_kw - (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) |