console.log

% make -f Makefile.dune coq
dune build --build-dir=_build_boot  @vodeps
dune exec --build-dir=_build_boot -- ./tools/coq_dune.exe _build_boot/default/.vfiles.d
dune build  coq.install
File "./theories/Init/Tauto.v", line 16, characters 7-8:
Error:
Syntax error: [rightwards_double_arrow] expected after '_' (in [match_context_rule]).

make: *** [Makefile.dune:63: coq] Error 1

gistfile1.patch

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 50c3ed1248..74fd851bc2 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -255,8 +255,9 @@ GRAMMAR EXTEND Gram
         "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
       | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
         "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) }
-      | "_"; "=>"; te = tactic_expr -> { All te } ] ]
+      | "_"; rightwards_double_arrow; te = tactic_expr -> { All te } ] ]
   ;
+  rightwards_double_arrow: [ [ "=>" -> { () } ] ] ;
   match_context_list:
     [ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl }
       | "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ]