Revert to "using" not being a keyword in -noinit mode.

The IDENT annotations in g_ltac.mlg are required to not break the
parser.

1 files changed, 2 insertions, 2 deletions

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index bd46e24a1c..c2e95c45f9 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -329,9 +329,9 @@ GRAMMAR EXTEND Gram
   ;
   command:
     [ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
-        l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] ->
+        l = OPT [ IDENT "using"; l = G_vernac.section_subset_expr -> { l } ] ->
           { Vernacexpr.VernacProof (Some (in_tac ta), l) }
-      | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
+      | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr;
         "with"; ta = Pltac.tactic ->
           { Vernacexpr.VernacProof (Some (in_tac ta),Some l) } ] ]
   ;