package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
doc/ltac_plugin/Ltac_plugin/Tacarg/index.html
Module Ltac_plugin.TacargSource
Source
val wit_intropattern :
(Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t,
Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t,
Tacexpr.intro_pattern)
Genarg.genarg_typeTactic related witnesses, could also live in tactics/ if other users
Source
val wit_simple_intropattern :
(Constrexpr.constr_expr Tactypes.intro_pattern_expr CAst.t,
Genintern.glob_constr_and_expr Tactypes.intro_pattern_expr CAst.t,
Tacexpr.intro_pattern)
Genarg.genarg_typeSource
val wit_open_constr_with_bindings :
(Constrexpr.constr_expr Tactypes.with_bindings,
Genintern.glob_constr_and_expr Tactypes.with_bindings,
EConstr.constr Tactypes.with_bindings Tactypes.delayed_open)
Genarg.genarg_typeGeneric arguments based on Ltac.
Source
val wit_tactic :
(Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t)
Genarg.genarg_typewit_ltac is subtly different from wit_tactic: they only change for their toplevel interpretation. The one of wit_ltac forces the tactic and discards the result.