diff options
| author | Jim Fehrle | 2020-04-12 11:47:13 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-04-12 11:47:13 -0700 |
| commit | 21a4d14307a9590c6b70e22383f96679012b5f4d (patch) | |
| tree | dec38d46571725da85b34b59e2ba4fd9a8e1c49a | |
| parent | 227520b14e978e19d58368de873521a283aecedd (diff) | |
Tweak grammar to make doc_grammar happy
| -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]) } ] |