package coq-core
Install
Dune Dependency
Authors
Maintainers
Sources
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
doc/ltac_plugin/Ltac_plugin/Tacentries/index.html
Module Ltac_plugin.TacentriesSource
Ltac toplevel command entries.
Tactic Definitions
val register_ltac :
Vernacexpr.locality_flag ->
?deprecation:Deprecation.t ->
Tacexpr.tacdef_body list ->
unitAdds 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
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.
A fully resolved argument type given as an AST with generic arguments on the leaves.
val add_tactic_notation :
?deprecation:Deprecation.t ->
tactic_grammar_obj ->
Tacexpr.raw_tactic_expr ->
unitadd_tactic_notation local level prods expr adds a tactic notation in the environment at level level with locality local made of the grammar productions prods and returning the body expr
val add_tactic_notation_syntax :
Vernacexpr.locality_flag ->
int ->
?deprecation:Deprecation.t ->
raw_argument grammar_tactic_prod_item_expr list ->
tactic_grammar_objRegister an argument under a given entry name for tactic notations. When translating raw_argument into argument, atomic names will be first looked up according to names registered through this function and fallback to finding an argument by name (as in Genarg) 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 ->
unitA low-level variant of add_tactic_notation used by the TACTIC EXTEND ML-side macro.
Tactic Quotations
val create_ltac_quotation :
plugin:string ->
string ->
('grm Loc.located -> Tacexpr.raw_tactic_arg) ->
('grm Pcoq.Entry.t * int option) ->
unitcreate_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 using f on the entry parsed by e.
Queries
Display the list of ltac definitions currently available.
Display the absolute name of a tactic.
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 ->
unitHelper 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 the ml_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 ->
unitSame 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
val tactic_extend :
string ->
string ->
level:Int.t ->
?deprecation:Deprecation.t ->
ty_ml list ->
unitval eval_of_ty_ml :
ty_ml ->
Geninterp.Val.t list ->
Geninterp.interp_sign ->
unit Proofview.tacticval clause_of_ty_ml :
ty_ml ->
Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr listgrammar rule for add_tactic_notation
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_printertype ('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 Gensubst.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| ArgInterpSimple : (Geninterp.interp_sign -> Environ.env -> Evd.evar_map -> 'b -> '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 :
plugin:string ->
name:string ->
('a, 'b, 'c) tactic_argument ->
('a, 'b, 'c) Genarg.genarg_type * 'a Pcoq.Entry.t