diff options
| author | Hugo Herbelin | 2020-05-02 23:22:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-06 17:04:11 +0200 |
| commit | 20f0e2efb87541e511cf31e220a44e4376c44550 (patch) | |
| tree | b08810a8fb0d6ac422b88e49f37a06ffd4dce550 | |
| parent | 86cdd51c4e25fceb12854863419fbdc3f19e44aa (diff) | |
Moving lazymatch and multimatch to simple identifiers.
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 3 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 4 |
2 files changed, 3 insertions, 4 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index dc994fe863..90173d65bf 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -57,8 +57,7 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: - - The grammar reserves the keywords ``lazymatch`` and - ``multimatch`` as well as the token ``||``. + - The grammar reserves the token ``||``. - The infix tacticals ``… || …`` , ``… + …`` , and ``… ; …`` are associative. diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 5baa23b3e9..0dea4fcc43 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -216,8 +216,8 @@ GRAMMAR EXTEND Gram ; match_key: [ [ "match" -> { Once } - | "lazymatch" -> { Select } - | "multimatch" -> { General } ] ] + | IDENT "lazymatch" -> { Select } + | IDENT "multimatch" -> { General } ] ] ; input_fun: [ [ "_" -> { Name.Anonymous } |