Module Synterp

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 =
| ControlTime of {
synterp_duration : System.duration;
}
| ControlInstructions of {
synterp_instructions : System.instruction_count;
}
| ControlRedirect of string
| ControlTimeout of {
remaining : float;
}
| ControlFail of {
st : Vernacstate.Synterp.t;
}
| ControlSucceed of {
st : Vernacstate.Synterp.t;
}
type synterp_entry =
| EVernacNoop
| EVernacNotation of {
local : bool;
decl : Metasyntax.notation_interpretation_decl;
}
| EVernacBeginSection of Names.lident
| EVernacEndSegment of Names.lident
| EVernacRequire of Library.library_t list * Names.DirPath.t list * Vernacexpr.export_with_cats option * (Libnames.qualid * Vernacexpr.import_filter_expr) list
| EVernacImport of Vernacexpr.export_flag * Libobject.open_filter * (Names.ModPath.t CAst.t * Vernacexpr.import_filter_expr) list
| EVernacDeclareModule of Lib.export * Names.lident * Declaremods.module_params_expr * module_entry
| 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
| EVernacDeclareModuleType of Names.lident * Declaremods.module_params_expr * ((Vernacexpr.export_flag * Libobject.open_filter) * Names.ModPath.t) list * module_entry list * module_entry list
| EVernacInclude of Declaremods.module_expr list
| EVernacSetOption of {
export : bool;
key : Goptions.option_name;
value : Vernacexpr.option_setting;
}
| EVernacLoad of Vernacexpr.verbose_flag * (vernac_control_entry * Vernacstate.Synterp.t) list
| 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
val synterp_require : Libnames.qualid option -> Vernacexpr.export_with_cats option -> (Libnames.qualid * Vernacexpr.import_filter_expr) list -> Library.library_t list * Names.DirPath.t list

synterp_require performs the syntactic interpretation phase of `Require` commands

val synterp_control : Vernacexpr.vernac_control -> vernac_control_entry

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 Stdlib.ref

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