From 2d6461140fadf1af8b92567b77e869eb2bd9dd7e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 26 Jul 2017 22:41:55 +0200
Subject: Tentative fix of parsing of product types.

---
 src/g_ltac2.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 88a64dacd9..cd227a78f1 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -121,7 +121,7 @@ GEXTEND Gram
     [ "5" RIGHTA
       [ t1 = tac2type; "->"; t2 = tac2type -> CTypArrow (!@loc, t1, t2) ]
     | "2"
-      [ t = tac2type; "*"; tl = LIST1 tac2type SEP "*" -> CTypTuple (!@loc, t :: tl) ]
+      [ t = tac2type; "*"; tl = LIST1 tac2type LEVEL "1" SEP "*" -> CTypTuple (!@loc, t :: tl) ]
     | "1" LEFTA
       [ t = SELF; qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [t]) ]
     | "0"
-- 
cgit v1.2.3