diff options
| author | Pierre-Marie Pédrot | 2020-04-23 14:49:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-23 14:49:58 +0200 |
| commit | 7863c12930687e1e2dc982d9b406fb4d6e7a02c1 (patch) | |
| tree | 957bd8b46b1c2d9dbbd4fbb25fa0877cb2aae278 | |
| parent | 7e2167f5bfd7d70847d1b1ece34c1f0303f46fc8 (diff) | |
| parent | 21a4d14307a9590c6b70e22383f96679012b5f4d (diff) | |
Merge PR #12083: Tweak ltac2 grammar to make doc_grammar happy
Reviewed-by: ppedrot
| -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]) } ] |