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

---
 test-suite/bugs/closed/bug_10116.v | 3 +++
 user-contrib/Ltac2/g_ltac2.mlg     | 6 +++---
 2 files changed, 6 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_10116.v

diff --git a/test-suite/bugs/closed/bug_10116.v b/test-suite/bugs/closed/bug_10116.v
new file mode 100644
index 0000000000..58caa59786
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10116.v
@@ -0,0 +1,3 @@
+From Ltac2 Require Import Ltac2.
+
+Ltac2 Eval true :: [], false.
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