package coq-core

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Vernac Translation into the Vernac DSL

val vernac_require : Libnames.qualid option -> Vernacexpr.export_with_cats option -> (Libnames.qualid * Vernacexpr.import_filter_expr) list -> unit

Vernacular require command, used by the command line

val vernac_require_interp : Library.library_t list -> Names.DirPath.t list -> Vernacexpr.export_with_cats option -> (Libnames.qualid * Vernacexpr.import_filter_expr) list -> unit

Interp phase of the require command

Hook to dissappear when #8240 is fixed

val command_focus : unit Proof.focus_kind

Miscellaneous stuff

val allow_sprop_opt_name : string list
module Preprocessed_Mind_decl : sig ... end

pre-processing and validation of VernacInductive

OCaml

Innovation. Community. Security.