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.

---
 plugins/ltac/g_ltac.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

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