2 files changed, 45 insertions, 0 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 32c61378db..48d4165830 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2613,3 +2613,30 @@ let vernac_extend ~command ?classifier ?entry ext =
   in
   let () = declare_vernac_classifier command cl in
   List.iteri iter ext
+
+(** VERNAC ARGUMENT EXTEND registering *)
+
+type 'a argument_rule =
+| Arg_alias of 'a Pcoq.Entry.t
+| Arg_rules of 'a Extend.production_rule list
+
+type 'a vernac_argument = {
+  arg_printer : 'a -> Pp.t;
+  arg_parsing : 'a argument_rule;
+}
+
+let vernac_argument_extend ~name arg =
+  let wit = Genarg.create_arg name in
+  let entry = match arg.arg_parsing with
+  | Arg_alias e ->
+    let () = Pcoq.register_grammar wit e in
+    e
+  | 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
+    e
+  in
+  let pr = arg.arg_printer in
+  let pr x = Genprint.PrinterBasic (fun () -> pr x) in
+  let () = Genprint.register_vernac_print0 wit pr in
+  (wit, entry)
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 34f6029e78..0c4630e45f 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -63,6 +63,24 @@ val vernac_extend :
   ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
   ty_ml list -> unit
 
+(** {5 VERNAC ARGUMENT EXTEND} *)
+
+type 'a argument_rule =
+| Arg_alias of 'a Pcoq.Entry.t
+  (** This is used because CAMLP5 parser can be dumb about rule factorization,
+      which sometimes requires two entries to be the same. *)
+| Arg_rules of 'a Extend.production_rule list
+  (** There is a discrepancy here as we use directly extension rules and thus
+    entries instead of ty_user_symbol and thus arguments as roots. *)
+
+type 'a vernac_argument = {
+  arg_printer : 'a -> Pp.t;
+  arg_parsing : 'a argument_rule;
+}
+
+val vernac_argument_extend : name:string -> 'a vernac_argument ->
+  ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t
+
 (** {5 STM classifiers} *)
 
 val get_vernac_classifier :