package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/coq-core.vernac/Vernacentries/index.html
Module VernacentriesSource
Source
val check_may_eval :
Environ.env ->
Evd.evar_map ->
Genredexpr.raw_red_expr option ->
Constrexpr.constr_expr ->
Pp.tSource
val translate_vernac :
?loc:Loc.t ->
atts:Attributes.vernac_flags ->
Synterp.vernac_entry ->
Vernacextend.typed_vernacVernac Translation into the Vernac DSL
Source
val vernac_require :
Libnames.qualid option ->
Vernacexpr.export_with_cats option ->
(Libnames.qualid * Vernacexpr.import_filter_expr) list ->
unitVernacular require command, used by the command line
Source
val vernac_require_interp :
Library.library_t list ->
Names.DirPath.t list ->
Vernacexpr.export_with_cats option ->
(Libnames.qualid * Vernacexpr.import_filter_expr) list ->
unitInterp phase of the require command
Source
val interp_redexp_hook :
(Environ.env ->
Evd.evar_map ->
Genredexpr.raw_red_expr ->
Evd.evar_map * Redexpr.red_expr)
Hook.tHook to dissappear when #8240 is fixed
Miscellaneous stuff
pre-processing and validation of VernacInductive
Source
val preprocess_inductive_decl :
atts:Attributes.vernac_flags ->
Vernacexpr.inductive_kind ->
(Vernacexpr.inductive_expr * Vernacexpr.notation_declaration list) list ->
Preprocessed_Mind_decl.t