diff options
| -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 } ] ] |