diff options
| author | Pierre-Marie Pédrot | 2020-06-26 09:49:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-01 13:33:08 +0200 |
| commit | 4e498fa2c96f4217c2d1204ebc032f224f93dbc4 (patch) | |
| tree | 1bfd2d4cade038162c9c82c0f3ddf79ca7266135 /user-contrib | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
Factorize tac2type syntax to fix the parsing of (t1, ..., tn) t.
It seems that nobody tried to write a parameterized type with more than one
parameter since this was causing a syntax error. LL(1) being great, we work
around the issue by factorizing the syntax with the generic parentheses and
decide the validity after parsing.
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 3af39ec59a..bec9632e84 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -262,12 +262,16 @@ GRAMMAR EXTEND Gram | "1" LEFTA [ t = SELF; qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, [t]) } ] | "0" - [ "("; t = tac2type LEVEL "5"; ")" -> { t } + [ "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = OPT Prim.qualid -> + { match p, qid with + | [t], None -> t + | _, None -> CErrors.user_err ~loc (Pp.str "Syntax error") + | ts, Some qid -> CAst.make ~loc @@ CTypRef (RelId qid, p) + } | id = typ_param -> { CAst.make ~loc @@ CTypVar (Name id) } | "_" -> { CAst.make ~loc @@ CTypVar Anonymous } | qid = Prim.qualid -> { CAst.make ~loc @@ CTypRef (RelId qid, []) } - | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid -> - { CAst.make ~loc @@ CTypRef (RelId qid, p) } ] + ] ]; locident: [ [ id = Prim.ident -> { CAst.make ~loc id } ] ] |