diff options
| author | Pierre-Marie Pédrot | 2017-08-07 16:22:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-07 16:24:09 +0200 |
| commit | c0f72bb07442075ee1dc66b4902b5c4681d220cf (patch) | |
| tree | fdfa699480af30d67f9642edf8d817158af92ccd | |
| parent | e1ea058fb664be58371237e5a6dbe0ec570448d5 (diff) | |
Fix parsing of parenthesized expressions.
| -rw-r--r-- | src/g_ltac2.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 8b373647f3..1cab918ea4 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -119,8 +119,8 @@ GEXTEND Gram | e = SELF; ".("; qid = Prim.qualid; ")" -> CTacPrj (!@loc, e, RelId qid) | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "5" -> CTacSet (!@loc, e, RelId qid, r) ] | "0" - [ "("; a = tac2expr LEVEL "5"; ")" -> a - | "("; a = tac2expr; ":"; t = tac2type; ")" -> CTacCnv (!@loc, a, t) + [ "("; a = SELF; ")" -> a + | "("; a = SELF; ":"; t = tac2type; ")" -> CTacCnv (!@loc, a, t) | "()" -> CTacCst (!@loc, AbsKn (Tuple 0)) | "("; ")" -> CTacCst (!@loc, AbsKn (Tuple 0)) | "["; a = LIST0 tac2expr LEVEL "5" SEP ";"; "]" -> CTacLst (Loc.tag ~loc:!@loc a) |