package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
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 ->
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 :
?deprecation:Deprecation.t ->
?local:bool ->
Tac2expr.sexpr list ->
int option ->
Tac2expr.raw_tacexpr ->
unitNotations
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.
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.t