From a647c38d3024f34711fbaa66975b5812097c33cc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Jul 2017 19:29:09 +0200
Subject: Properly handle parsing of list patterns.

---
 src/g_ltac2.ml4 | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 36057b3a67..6cdbccb11d 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -33,7 +33,11 @@ GEXTEND Gram
   tac2pat:
     [ "1" LEFTA
       [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> CPatRef (!@loc, RelId id, pl)
-      | id = Prim.qualid -> CPatRef (!@loc, RelId id, []) ]
+      | id = Prim.qualid -> CPatRef (!@loc, RelId id, [])
+      | "["; "]" -> CPatRef (!@loc, AbsKn Tac2core.Core.c_nil, [])
+      | p1 = tac2pat; "::"; p2 = tac2pat ->
+        CPatRef (!@loc, AbsKn Tac2core.Core.c_cons, [p1; p2])
+      ]
     | "0"
       [ "_" -> CPatAny (!@loc)
       | "()" -> CPatTup (Loc.tag ~loc:!@loc [])
-- 
cgit v1.2.3