package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
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