package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/rocq-runtime.vernac/Synterp/index.html

Module SynterpSource

This module implements the syntactic interpretation phase of vernacular commands. The main entry point is synterp_control, which transforms a vernacexpr into a vernac_control_entry.

Sourceval module_locality : bool Attributes.attribute
Sourceval with_locality : atts:Attributes.vernac_flags -> (local:bool option -> 'a) -> 'a
Sourceval with_module_locality : atts:Attributes.vernac_flags -> (module_local:bool -> 'a) -> 'a
Sourceval with_generic_atts : check:bool -> Attributes.vernac_flags -> (atts:Attributes.vernac_flags -> 'a) -> 'a
Sourcetype module_entry = Modintern.module_struct_expr * Names.ModPath.t * Modintern.module_kind * Entries.inline
Sourcetype synterp_entry =
  1. | EVernacNoop
  2. | EVernacNotation of {
    1. local : bool;
    2. decl : Metasyntax.notation_interpretation_decl;
    }
  3. | EVernacBeginSection of Names.lident
  4. | EVernacEndSegment of Names.lident
  5. | EVernacRequire of Library.library_t list * Names.DirPath.t list * Vernacexpr.export_with_cats option * (Libnames.qualid * Vernacexpr.import_filter_expr) list
  6. | EVernacImport of Vernacexpr.export_flag * Libobject.open_filter * (Names.ModPath.t CAst.t * Vernacexpr.import_filter_expr) list
  7. | EVernacDeclareModule of Lib.export * Names.lident * Declaremods.module_params_expr * module_entry
  8. | EVernacDefineModule of Lib.export * Names.lident * Declaremods.module_params_expr * ((Vernacexpr.export_flag * Libobject.open_filter) * Names.ModPath.t) list * module_entry Declaremods.module_signature * module_entry list
  9. | EVernacDeclareModuleType of Names.lident * Declaremods.module_params_expr * ((Vernacexpr.export_flag * Libobject.open_filter) * Names.ModPath.t) list * module_entry list * module_entry list
  10. | EVernacInclude of Declaremods.module_expr list
  11. | EVernacSetOption of {
    1. export : bool;
    2. key : Goptions.option_name;
    3. value : Vernacexpr.option_setting;
    }
  12. | EVernacLoad of Vernacexpr.verbose_flag * (vernac_control_entry * Vernacstate.Synterp.t) list
  13. | EVernacExtend of Vernactypes.typed_vernac
Sourceand vernac_entry = synterp_entry Vernacexpr.vernac_expr_gen
Sourceand vernac_control_entry = (Vernacstate.Synterp.t VernacControl.control_entry, synterp_entry) Vernacexpr.vernac_control_gen_r CAst.t

vernac_control_entry defines elaborated vernacular expressions, after the syntactic interpretation phase and before full interpretation

Sourceexception UnmappedLibrary of Names.DirPath.t option * Libnames.qualid
Sourceexception NotFoundLibrary of Names.DirPath.t option * Libnames.qualid

synterp_require performs the syntactic interpretation phase of `Require` commands

synterp_control is the main entry point of the syntactic interpretation phase

Sourceval get_default_proof_mode : unit -> Pvernac.proof_mode

Default proof mode set by `start_proof`