Module `Pvernac`

val uvernac : Pcoq.gram_universe

type proof_mode

module Vernac_ : sig ... end

module Unsafe : sig ... end

val main_entry : proof_mode option -> Vernacexpr.vernac_control CAst.t option Pcoq.Entry.t: The main entry: reads an optional vernac command

val register_proof_mode : string -> Vernacexpr.vernac_expr Pcoq.Entry.t -> proof_mode
val lookup_proof_mode : string -> proof_mode option
val proof_mode_to_string : proof_mode -> string