diff options
| author | Hugo Herbelin | 2019-11-13 17:18:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-06 17:04:11 +0200 |
| commit | 62f6fb862ce4f3eec46200d11e503aa5d6d051db (patch) | |
| tree | 323b0a77e1f0dbf2e07067b65fc0f359f1d00ff2 /vernac | |
| parent | bc79d319d38f766a6b7bbeb1f1071b046642089b (diff) | |
Documenting plugin/tactic/stdlib keywords in corresponding chapters.
Incidentally removing "discriminated", "(bfs)" and "(dfs)" from
keywords. It is enough to make them normal identifiers.
Note:
- keywords reserved by the tactics are: ** [= _eqn |- by using
- keywords reserved by ltac are: lazymatch multimatch ||
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) } |