diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 6 |
1 files changed, 5 insertions, 1 deletions
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 []) |