diff options
| -rw-r--r-- | contrib/subtac/g_subtac.ml4 | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 337cc09fc1..933ea94b31 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -67,10 +67,12 @@ GEXTEND Gram Constr.binder: [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], c, p)]) in - ([id], typ) ] ]; - - + ([id],mkAppC (sigref, [mkLambdaC ([id], c, p)])) + | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" -> + ([id],c) + | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" -> + (id::lid,c) + ] ]; END |