package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val uvernac : Pcoq.gram_universe
  • deprecated Deprecated in 8.13
type proof_mode
module Vernac_ : sig ... end
module Unsafe : sig ... end
val main_entry : proof_mode option -> Vernacexpr.vernac_control option Pcoq.Entry.t
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