package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2
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 :
intern:Library.Intern.t ->
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
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