[parsing] Track need to reinit by typing

This PR is in preparation of #9067 (together with #11647) .

Before this PR, `grammar_extend` always took an optional `reinit`
argument, even if it was never set to `Some ...`. Indeed, there is a
single case where reinit is needed; we track it now by using a
different extension rule constructor.

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 13a2f3b8c0..8b4520947b 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -191,7 +191,7 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in
-  let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in
+  let r = ExtendRule (entry, (pos, [(None, None, [rules])])) in
   ([r], state)
 
 let tactic_grammar =
@@ -415,7 +415,7 @@ let create_ltac_quotation name cast (e, l) =
   in
   let action _ v _ _ _ loc = cast (Some loc, v) in
   let gram = (level, assoc, [Rule (rule, action)]) in
-  Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram])
+  Pcoq.grammar_extend Pltac.tactic_arg (None, [gram])
 
 (** Command *)
 
@@ -759,7 +759,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
     e
   | Vernacextend.Arg_rules rules ->
     let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
-    let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in
+    let () = Pcoq.grammar_extend e (None, [(None, None, rules)]) in
     e
   in
   let (rpr, gpr, tpr) = arg.arg_printer in