Module Ltac_plugin.Tacentries
Tactic Definitions
val register_ltac : Vernacexpr.locality_flag -> ?deprecation:Deprecation.t -> Tacexpr.tacdef_body list -> unit
Adds new Ltac definitions to the environment.
Tactic Notations
type 'a grammar_tactic_prod_item_expr
= 'a Pptactic.grammar_tactic_prod_item_expr
=
|
TacTerm of string
|
TacNonTerm of ('a * Names.Id.t option) Loc.located
type raw_argument
= string * string option
An argument type as provided in Tactic notations, i.e. a string like "ne_foo_list_opt" together with a separator that only makes sense in the "_sep" cases.
type argument
= Genarg.ArgT.any Extend.user_symbol
A fully resolved argument type given as an AST with generic arguments on the leaves.
val add_tactic_notation : Vernacexpr.locality_flag -> int -> ?deprecation:Deprecation.t -> raw_argument grammar_tactic_prod_item_expr list -> Tacexpr.raw_tactic_expr -> unit
add_tactic_notation local level prods expr
adds a tactic notation in the environment at levellevel
with localitylocal
made of the grammar productionsprods
and returning the bodyexpr
val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -> unit
Register an argument under a given entry name for tactic notations. When translating
raw_argument
intoargument
, atomic names will be first looked up according to names registered through this function and fallback to finding an argument by name (as inGenarg
) if there is none matching.
val add_ml_tactic_notation : Tacexpr.ml_tactic_name -> level:int -> ?deprecation:Deprecation.t -> argument grammar_tactic_prod_item_expr list list -> unit
A low-level variant of
add_tactic_notation
used by the TACTIC EXTEND ML-side macro.
Tactic Quotations
val create_ltac_quotation : string -> ('grm Loc.located -> Tacexpr.raw_tactic_arg) -> ('grm Pcoq.Entry.t * int option) -> unit
create_ltac_quotation name f e
adds a quotation rule to Ltac, that is, Ltac grammar now accepts arguments of the form"name" ":" "(" <e> ")"
, and generates an argument usingf
on the entry parsed bye
.
Queries
val print_located_tactic : Libnames.qualid -> unit
Display the absolute name of a tactic.
val print_ltac : Libnames.qualid -> Pp.t
Display the definition of a tactic.
Low-level registering of tactics
type (_, 'a) ml_ty_sig
=
|
MLTyNil : ('a, 'a) ml_ty_sig
|
MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig
val ml_tactic_extend : plugin:string -> name:string -> local:Vernacexpr.locality_flag -> ?deprecation:Deprecation.t -> ('r, unit Proofview.tactic) ml_ty_sig -> 'r -> unit
Helper function to define directly an Ltac function in OCaml without any associated parsing rule nor further shenanigans. The Ltac function will be defined as
name
in the Coq file that loads the ML plugin where this function is called. It will have the arity given by theml_ty_sig
argument.
val ml_val_tactic_extend : plugin:string -> name:string -> local:Vernacexpr.locality_flag -> ?deprecation:Deprecation.t -> ('r, Geninterp.Val.t Ftactic.t) ml_ty_sig -> 'r -> unit
Same as
ml_tactic_extend
but the function can return an argument instead.
TACTIC EXTEND
type _ ty_sig
=
|
TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
|
TyIdent : string * 'r ty_sig -> 'r ty_sig
|
TyArg : ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> ('c -> 'r) ty_sig
type ty_ml
=
|
TyML : 'r ty_sig * 'r -> ty_ml
val tactic_extend : string -> string -> level:Int.t -> ?deprecation:Deprecation.t -> ty_ml list -> unit
val eval_of_ty_ml : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic
val clause_of_ty_ml : ty_ml -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
grammar rule for
add_tactic_notation
ARGUMENT EXTEND
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 -> Goal.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp
type ('a, 'b, 'c) tactic_argument
=
{
arg_parsing : 'a Vernacextend.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