From 21a4d14307a9590c6b70e22383f96679012b5f4d Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 12 Apr 2020 11:47:13 -0700
Subject: Tweak grammar to make doc_grammar happy

---
 user-contrib/Ltac2/g_ltac2.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 57d59fc2ef..13c4d667a0 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -145,10 +145,10 @@ GRAMMAR EXTEND Gram
         { CAst.make ~loc @@ CTacCse (e, bl) }
       ]
     | "4" LEFTA [ ]
-    | [ e0 = SELF; ","; el = LIST1 NEXT SEP "," ->
+    | "3" [ e0 = SELF; ","; el = LIST1 NEXT SEP "," ->
         { let el = e0 :: el in
           CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) } ]
-    | "::" RIGHTA
+    | "2" RIGHTA
       [ e1 = tac2expr; "::"; e2 = tac2expr ->
         { CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2]) }
       ]
-- 
cgit v1.2.3