package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
val vernac_require : Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> st:Vernacstate.t -> Vernacexpr.vernac_control CAst.t -> Vernacstate.t
val make_cases : string -> string list list
val with_fail : Vernacstate.t -> bool -> (unit -> unit) -> unit
val command_focus : unit Proof.focus_kind
val universe_polymorphism_option_name : string list
val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts
type (!_, !_) ty_sig =
  1. | TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
  2. | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
  3. | TyNonTerminal : string option * ('a, 'b, 'c) Extend.ty_user_symbol * ('r0, 's0) ty_sig -> ('a -> 'r0, 'a -> 's0) ty_sig
type ty_ml =
  1. | TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
val vernac_extend : command:string -> ?classifier:(string -> Vernacexpr.vernac_classification) -> ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> ty_ml list -> unit
val get_vernac_classifier : Vernacexpr.extend_name -> classifier
val declare_vernac_classifier : string -> classifier array -> unit