package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824
doc/rocq-runtime.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