diff options
| author | Pierre-Marie Pédrot | 2017-07-24 19:29:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-24 19:29:42 +0200 |
| commit | a647c38d3024f34711fbaa66975b5812097c33cc (patch) | |
| tree | 7448bb021fb7a3a64039a129643cb9e8a766acf5 /src | |
| parent | 1fe83d5d791f0ff91ffa032b556f02c6cc4cbfed (diff) | |
Properly handle parsing of list patterns.
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 []) |