package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b
doc/ltac2_plugin/Ltac2_plugin/Tac2entries/index.html
Module Ltac2_plugin.Tac2entriesSource
Toplevel definitions
Source
val register_ltac :
?deprecation:Deprecation.t ->
?local:bool ->
?mut:bool ->
Tac2expr.rec_flag ->
(Names.lname * Tac2expr.raw_tacexpr) list ->
unitSource
val register_type :
?local:bool ->
?abstract:bool ->
Tac2expr.rec_flag ->
(Libnames.qualid * Tac2expr.redef_flag * Tac2expr.raw_quant_typedef) list ->
unitSource
val register_primitive :
?deprecation:Deprecation.t ->
?local:bool ->
Names.lident ->
Tac2expr.raw_typexpr ->
Tac2expr.ml_tactic_name ->
unitSource
val register_notation :
Attributes.vernac_flags ->
Tac2expr.sexpr list ->
int option ->
Tac2expr.raw_tacexpr ->
notation_interpretation_dataNotations
Source
type scope_rule = | ScopeRule : (Tac2expr.raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> Tac2expr.raw_tacexpr) -> scope_rule
Create a new scope with the provided name
Use this to interpret the subscopes for interpretation functions
Inspecting
Display the absolute name of a tactic.
Display the definition of a tactic.
Display the definition of a type.
Print types of all definitions in scope.
Eval loop
Source
val call :
pstate:Declare.Proof.t ->
Goal_select.t option ->
with_end_tac:bool ->
Tac2expr.raw_tacexpr ->
Declare.Proof.tEvaluate a tactic expression in the current environment
Source
val call_par :
pstate:Declare.Proof.t ->
with_end_tac:bool ->
Tac2expr.raw_tacexpr ->
Declare.Proof.tParsing entries
On This Page