Allow ARGUMENT EXTEND grammar to be printed with Print Grammar.

coq · Oct 4, 2020 · 4e338a5 · 4e338a5
1 parent ad531e6
commit 4e338a5
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
@@ -870,6 +870,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
+    register_grammars_by_name name [AnyEntry e];
     e
   in
   let (rpr, gpr, tpr) = arg.arg_printer in