Add support for Proof using in -noinit mode.

"Proof with" is Ltac-specific but there is no reason why it should be
the same for "Proof using".

1 files changed, 2 insertions, 2 deletions

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c54f8ffa78..bd46e24a1c 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -332,8 +332,8 @@ GRAMMAR EXTEND Gram
         l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] ->
           { Vernacexpr.VernacProof (Some (in_tac ta), l) }
       | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
-        ta = OPT [ "with"; ta = Pltac.tactic -> { in_tac ta } ] ->
-          { Vernacexpr.VernacProof (ta,Some l) } ] ]
+        "with"; ta = Pltac.tactic ->
+          { Vernacexpr.VernacProof (Some (in_tac ta),Some l) } ] ]
   ;
   hint:
     [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";