diff options
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 57d59fc2ef..13c4d667a0 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -145,10 +145,10 @@ GRAMMAR EXTEND Gram { CAst.make ~loc @@ CTacCse (e, bl) } ] | "4" LEFTA [ ] - | [ e0 = SELF; ","; el = LIST1 NEXT SEP "," -> + | "3" [ e0 = SELF; ","; el = LIST1 NEXT SEP "," -> { let el = e0 :: el in CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Tuple (List.length el))), el) } ] - | "::" RIGHTA + | "2" RIGHTA [ e1 = tac2expr; "::"; e2 = tac2expr -> { CAst.make ~loc @@ CTacApp (CAst.make ~loc @@ CTacCst (AbsKn (Other Tac2core.Core.c_cons)), [e1; e2]) } ] |