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