Module `Synterp`Source

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

Source

val with_locality : 
  atts:Attributes.vernac_flags ->
  (local:bool option -> 'a) ->
  'a

Source

val with_module_locality : 
  atts:Attributes.vernac_flags ->
  (module_local:bool -> 'a) ->
  'a

Source

val with_generic_atts : 
  check:bool ->
  Attributes.vernac_flags ->
  (atts:Attributes.vernac_flags -> 'a) ->
  'a

Source

type module_entry =
  Modintern.module_struct_expr
  * Names.ModPath.t
  * Modintern.module_kind
  * Entries.inline

Sourcetype synterp_entry =

| EVernacNoop
| EVernacNotation of {
1. local : bool;
2. 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 {
1. export : bool;
2. key : Goptions.option_name;
3. value : Vernacexpr.option_setting;
}
| EVernacLoad of Vernacexpr.verbose_flag * (vernac_control_entry * Vernacstate.Synterp.t) list
| EVernacExtend of Vernactypes.typed_vernac

Sourceand vernac_entry = synterp_entry Vernacexpr.vernac_expr_gen

Source

and vernac_control_entry =
  (Vernacstate.Synterp.t VernacControl.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

Source

val synterp_require : 
  intern:Library.Intern.t ->
  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

Source

val synterp_control : 
  intern:Library.Intern.t ->
  Vernacexpr.vernac_control ->
  vernac_control_entry

synterp_control is the main entry point of the syntactic interpretation phase

Sourceval get_default_proof_mode : unit -> Pvernac.proof_mode

Default proof mode set by `start_proof`

Sourceval proof_mode_opt_name : string list

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.vernac/Synterp/index.html

Module `Synterp`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.vernac/Synterp/index.html

Module SynterpSource

Module `Synterp`Source