package coq-core

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

Install 

dune-project
 Dependency

coq.inria.fr Readme 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.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

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. | ControlInstructions of {
    1. synterp_instructions : System.instruction_count;
    }
  3. | ControlRedirect of string
  4. | ControlTimeout of {
    1. remaining : float;
    }
  5. | ControlFail of {
    1. st : Vernacstate.Synterp.t;
    }
  6. | ControlSucceed of {
    1. st : Vernacstate.Synterp.t;
    }

Interprete control flag assuming a synpure command.

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 = (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 add_default_timeout : Vernacexpr.control_flag list -> Vernacexpr.control_flag list
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