From 4e498fa2c96f4217c2d1204ebc032f224f93dbc4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 26 Jun 2020 09:49:23 +0200
Subject: Factorize tac2type syntax to fix the parsing of (t1, ..., tn) t.

It seems that nobody tried to write a parameterized type with more than one
parameter since this was causing a syntax error. LL(1) being great, we work
around the issue by factorizing the syntax with the generic parentheses and
decide the validity after parsing.
---
 user-contrib/Ltac2/g_ltac2.mlg | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 3af39ec59a..bec9632e84 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -262,12 +262,16 @@ GRAMMAR EXTEND Gram
     | "1" LEFTA
       [ t = SELF; qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, [t]) } ]
     | "0"
-      [ "("; t = tac2type LEVEL "5"; ")"  -> { t }
+      [ "(";  p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid ->
+        { match p, qid with
+          | [t], None -> t
+          | _, None -> CErrors.user_err ~loc (Pp.str "Syntax error")
+          | ts, Some qid -> CAst.make ~loc @@ CTypRef (RelId qid, p)
+        }
       | id = typ_param -> { CAst.make ~loc @@ CTypVar (Name id) }
       | "_" -> { CAst.make ~loc @@ CTypVar Anonymous }
       | qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, []) }
-      | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid ->
-        { CAst.make ~loc @@ CTypRef (RelId qid, p) } ]
+      ]
     ];
   locident:
     [ [ id = Prim.ident -> { CAst.make ~loc id } ] ]
-- 
cgit v1.2.3


From 7bec233c0e5ea056c2d8cc5dbfc034b619a9f5dd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 26 Jun 2020 09:53:34 +0200
Subject: Add a test for Ltac2 parsing of parameterized types.

---
 test-suite/ltac2/syntax.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 test-suite/ltac2/syntax.v

diff --git a/test-suite/ltac2/syntax.v b/test-suite/ltac2/syntax.v
new file mode 100644
index 0000000000..872b2142d0
--- /dev/null
+++ b/test-suite/ltac2/syntax.v
@@ -0,0 +1,12 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 Type ('a, 'b, 'c) t.
+Ltac2 Type ('a) u.
+Ltac2 Type 'a v.
+
+Ltac2 foo
+  (f : ('a, 'b, 'c) t -> ('a -> 'a, 'b -> 'c, 'c * 'c) t)
+  (x : ('a, 'b, 'c) t) :=
+  f x.
+
+Ltac2 bar (x : 'a u) (y : ('b) v) := x.
-- 
cgit v1.2.3


From 810197a6577c7a4a40f406ae64f918f72e7d0012 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 26 Jun 2020 10:01:32 +0200
Subject: Add a changelog.

---
 doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst

diff --git a/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst
new file mode 100644
index 0000000000..555020d319
--- /dev/null
+++ b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Fix the parsing of multi-parameters Ltac2 types
+  (`#12594 <https://github.com/coq/coq/pull/12594>`_,
+  fixes `#12595 <https://github.com/coq/coq/issues/12595>`_,
+  by Pierre-Marie Pédrot).
-- 
cgit v1.2.3