package coq-core

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

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

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