Vernacentries (p.coq.8.14.1.doc.coq-core.vernac.Vernacentries)

val translate_vernac : 
  ?loc:Loc.t ->
  atts:Attributes.vernac_flags ->
  Vernacexpr.vernac_expr ->
  Vernacextend.typed_vernac

Vernac Translation into the Vernac DSL

val vernac_require : 
  Libnames.qualid option ->
  bool option ->
  Libnames.qualid list ->
  unit

Vernacular require command

val interp_redexp_hook : 
  (Environ.env ->
    Evd.evar_map ->
    Genredexpr.raw_red_expr ->
    Evd.evar_map * Redexpr.red_expr)
    Hook.t

Hook to dissappear when #8240 is fixed

Sourceval command_focus : unit Proof.focus_kind

Miscellaneous stuff

Sourceval allow_sprop_opt_name : string list