From 20f0e2efb87541e511cf31e220a44e4376c44550 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 2 May 2020 23:22:48 +0200
Subject: Moving lazymatch and multimatch to simple identifiers.

---
 doc/sphinx/proof-engine/ltac.rst | 3 +--
 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 }
-- 
cgit v1.2.3