package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

val module_locality : bool Attributes.attribute
val with_locality : atts:Attributes.vernac_flags -> (local:bool option -> 'a) -> 'a
val with_module_locality : atts:Attributes.vernac_flags -> (module_local:bool -> 'a) -> 'a
val with_generic_atts : check:bool -> Attributes.vernac_flags -> (atts:Attributes.vernac_flags -> 'a) -> 'a
type module_entry = Modintern.module_struct_expr * Names.ModPath.t * Modintern.module_kind * Entries.inline
type 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;
    }
type 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
and vernac_entry = synterp_entry Vernacexpr.vernac_expr_gen
and 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

exception UnmappedLibrary of Names.DirPath.t option * Libnames.qualid
exception 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

val get_default_proof_mode : unit -> Pvernac.proof_mode

Default proof mode set by `start_proof`

val proof_mode_opt_name : string list
val test_mode : bool ref

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct