package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val check_evars : Environ.env -> Evd.evar_map -> unit
val evar_dependencies : Evd.evar_map -> Evar.t -> Evar.Set.t
val sort_dependencies : (Evar.t * Evd.evar_info * Evar.Set.t) list -> (Evar.t * Evd.evar_info * Evar.Set.t) list
val default_tactic : unit Proofview.tactic ref
val add_definition : name:Names.Id.t -> ?term:Constr.constr -> Constr.types -> UState.t -> ?univdecl:UState.universe_decl -> ?implicits:Impargs.manual_implicits -> poly:bool -> ?scope:DeclareDef.locality -> ?kind:Decls.definition_object_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(Constr.constr -> Constr.constr) -> ?hook:DeclareDef.Hook.t -> ?opaque:bool -> obligation_info -> DeclareObl.progress
val add_mutual_definitions : (Names.Id.t * Constr.constr * Constr.types * Impargs.manual_implicits * obligation_info) list -> UState.t -> ?univdecl:UState.universe_decl -> ?tactic:unit Proofview.tactic -> poly:bool -> ?scope:DeclareDef.locality -> ?kind:Decls.definition_object_kind -> ?reduce:(Constr.constr -> Constr.constr) -> ?hook:DeclareDef.Hook.t -> ?opaque:bool -> Vernacexpr.decl_notation list -> DeclareObl.fixpoint_kind -> unit
val obligation : (int * Names.Id.t option * Constrexpr.constr_expr option) -> Genarg.glob_generic_argument option -> Lemmas.t
val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> Lemmas.t
val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> DeclareObl.progress
val solve_all_obligations : unit Proofview.tactic option -> unit
val try_solve_obligation : int -> Names.Id.t option -> unit Proofview.tactic option -> unit
val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> unit
val show_obligations : ?msg:bool -> Names.Id.t option -> unit
val show_term : Names.Id.t option -> Pp.t
val admit_obligations : Names.Id.t option -> unit
exception NoObligations of Names.Id.t option
val explain_no_obligations : Names.Id.t option -> Pp.t
val check_program_libraries : unit -> unit
OCaml

Innovation. Community. Security.