package coq-core

  1. Overview
  2. No Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (11)

Authors

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

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

doc/coq-core.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 control_entry =
  1. | ControlTime of {
    1. synterp_duration : System.duration;
    }
  2. | ControlRedirect of string
  3. | ControlTimeout of {
    1. remaining : float;
    }
  4. | ControlFail of {
    1. st : Vernacstate.Synterp.t;
    }
  5. | ControlSucceed of {
    1. st : Vernacstate.Synterp.t;
    }
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 Vernacextend.typed_vernac
Sourceand vernac_entry = synterp_entry Vernacexpr.vernac_expr_gen
Sourceand vernac_control_entry = (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`

Sourceval proof_mode_opt_name : string list
Sourceval test_mode : bool ref

Flag set when the test-suite is called. Its only effect to display verbose information for Fail