package coq-core

  1. Overview
  2. Docs
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 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;
    }
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.