diff options
| author | Pierre-Marie Pédrot | 2017-07-26 22:41:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-26 22:43:35 +0200 |
| commit | 2d6461140fadf1af8b92567b77e869eb2bd9dd7e (patch) | |
| tree | 7318ce7e1a4a44fa4ce59b703df44b42720d39fa /src | |
| parent | 57b9df4e07351a753f897dc24eb8238f6465b26d (diff) | |
Tentative fix of parsing of product types.
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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" |