3 files changed, 153 insertions, 1 deletions
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index ec96e1bbdd..e83eab20dc 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -7,10 +7,10 @@ Pltac
 Taccoerce
 Tactic_debug
 Tacintern
-Tacentries
 Profile_ltac
 Tactic_matching
 Tacinterp
+Tacentries
 Evar_tactics
 Tactic_option
 Extraargs
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index a77a9c2f45..16cff420bd 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -673,3 +673,96 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
   let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in
   Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
   Mltop.declare_cache_obj obj plugin_name
+
+
+(** ARGUMENT EXTEND *)
+
+open Geninterp
+
+type ('a, 'b, 'c) argument_printer =
+  'a Pptactic.raw_extra_genarg_printer *
+  'b Pptactic.glob_extra_genarg_printer *
+  'c Pptactic.extra_genarg_printer
+
+type ('a, 'b) argument_intern =
+| ArgInternFun : ('a, 'b) Genintern.intern_fun -> ('a, 'b) argument_intern
+| ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern
+
+type 'b argument_subst =
+| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst
+| ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst
+
+type ('b, 'c) argument_interp =
+| ArgInterpRet : ('c, 'c) argument_interp
+| ArgInterpFun : ('b, Val.t) interp_fun -> ('b, 'c) argument_interp
+| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
+| ArgInterpLegacy :
+  (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+
+type ('a, 'b, 'c) tactic_argument = {
+  arg_parsing : 'a Vernacentries.argument_rule;
+  arg_tag : 'c Val.tag option;
+  arg_intern : ('a, 'b) argument_intern;
+  arg_subst : 'b argument_subst;
+  arg_interp : ('b, 'c) argument_interp;
+  arg_printer : ('a, 'b, 'c) argument_printer;
+}
+
+let intern_fun (type a b c) name (arg : (a, b, c) tactic_argument) : (a, b) Genintern.intern_fun =
+match arg.arg_intern with
+| ArgInternFun f -> f
+| ArgInternWit wit ->
+  fun ist v ->
+    let ans = Genarg.out_gen (glbwit wit) (Tacintern.intern_genarg ist (Genarg.in_gen (rawwit wit) v)) in
+    (ist, ans)
+
+let subst_fun (type a b c) (arg : (a, b, c) tactic_argument) : b Genintern.subst_fun =
+match arg.arg_subst with
+| ArgSubstFun f -> f
+| ArgSubstWit wit ->
+  fun s v ->
+    let ans = Genarg.out_gen (glbwit wit) (Tacsubst.subst_genarg s (Genarg.in_gen (glbwit wit) v)) in
+    ans
+
+let interp_fun (type a b c) name (arg : (a, b, c) tactic_argument) (tag : c Val.tag) : (b, Val.t) interp_fun =
+match arg.arg_interp with
+| ArgInterpRet -> (fun ist v -> Ftactic.return (Geninterp.Val.inject tag v))
+| ArgInterpFun f -> f
+| ArgInterpWit wit ->
+  (fun ist x -> Tacinterp.interp_genarg ist (Genarg.in_gen (glbwit wit) x))
+| ArgInterpLegacy f ->
+  (fun ist v -> Ftactic.enter (fun gl ->
+    let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in
+    let v = Geninterp.Val.inject tag v in
+    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v)
+  ))
+
+let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
+  let wit = Genarg.create_arg name in
+  let () = Genintern.register_intern0 wit (intern_fun name arg) in
+  let () = Genintern.register_subst0 wit (subst_fun arg) in
+  let tag = match arg.arg_tag with
+  | None ->
+    let () = register_val0 wit None in
+    val_tag (topwit wit)
+  | Some tag ->
+    let () = register_val0 wit (Some tag) in
+    tag
+  in
+  let () = register_interp0 wit (interp_fun name arg tag) in
+  let entry = match arg.arg_parsing with
+  | Vernacentries.Arg_alias e ->
+    let () = Pcoq.register_grammar wit e in
+    e
+  | Vernacentries.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 (rpr, gpr, tpr) = arg.arg_printer in
+  let () = Pptactic.declare_extra_genarg_pprule wit rpr gpr tpr in
+  let () = create_ltac_quotation name
+    (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v))
+    (entry, None)
+  in
+  (wit, entry)
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 0b2b426018..5b4bedb50a 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -70,6 +70,8 @@ val print_ltacs : unit -> unit
 val print_located_tactic : Libnames.qualid -> unit
 (** Display the absolute name of a tactic. *)
 
+(** {5 TACTIC EXTEND} *)
+
 type _ ty_sig =
 | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
 | TyIdent : string * 'r ty_sig -> 'r ty_sig
@@ -79,3 +81,60 @@ type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
 
 val tactic_extend : string -> string -> level:Int.t ->
   ?deprecation:deprecation -> ty_ml list -> unit
+
+(** {5 ARGUMENT EXTEND} *)
+
+(**
+
+  This is the main entry point for the ARGUMENT EXTEND macro that allows to
+  easily create user-made Ltac arguments.
+
+
+  Each argument has three type parameters. See {!Genarg} for more details.
+  There are two kinds of Ltac arguments, uniform and non-uniform. The former
+  have the same type at each level (raw, glob, top) while the latter may vary.
+
+  When declaring an argument one must provide the following data:
+  - Internalization : raw -> glob
+  - Substitution : glob -> glob
+  - Interpretation : glob -> Ltac dynamic value
+  - Printing for every level
+  - An optional toplevel tag of type top (with the proviso that the
+    interpretation function only produces values with this tag)
+
+  This data can be either given explicitly with the [Fun] constructors, or it
+  can be inherited from another argument with the [Wit] constructors.
+
+*)
+
+type ('a, 'b, 'c) argument_printer =
+  'a Pptactic.raw_extra_genarg_printer *
+  'b Pptactic.glob_extra_genarg_printer *
+  'c Pptactic.extra_genarg_printer
+
+type ('a, 'b) argument_intern =
+| ArgInternFun : ('a, 'b) Genintern.intern_fun -> ('a, 'b) argument_intern
+| ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern
+
+type 'b argument_subst =
+| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst
+| ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst
+
+type ('b, 'c) argument_interp =
+| ArgInterpRet : ('c, 'c) argument_interp
+| ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c) argument_interp
+| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp
+| ArgInterpLegacy :
+  (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
+
+type ('a, 'b, 'c) tactic_argument = {
+  arg_parsing : 'a Vernacentries.argument_rule;
+  arg_tag : 'c Geninterp.Val.tag option;
+  arg_intern : ('a, 'b) argument_intern;
+  arg_subst : 'b argument_subst;
+  arg_interp : ('b, 'c) argument_interp;
+  arg_printer : ('a, 'b, 'c) argument_printer;
+}
+
+val argument_extend : name:string -> ('a, 'b, 'c) tactic_argument ->
+  ('a, 'b, 'c) Genarg.genarg_type * 'a Pcoq.Entry.t