From e3fb17911c74cfde61367c8558bd0926642280c9 Mon Sep 17 00:00:00 2001
From: Kenji Maillard
Date: Wed, 6 Nov 2019 22:17:14 +0100
Subject: Swap parsing precedence of `::` and `,` ; Fix #10116

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

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 9d4a3706f4..cc3a7c0f79 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -175,13 +175,13 @@ GRAMMAR EXTEND Gram
         { CAst.make ~loc @@ CTacCse (e, bl) }
       ]
     | "4" LEFTA [ ]
+    | [ 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
       [ e1 = tac2expr; "::"; e2 = tac2expr ->
         { CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2]) }
       ]
-    | [ 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) } ]
     | "1" LEFTA
       [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" ->
         { CAst.make ~loc @@ CTacApp (e, el) }
-- 
cgit v1.2.3