package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
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 ->
Vernactypes.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