package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t
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
type progress =
  1. | Remain of int
  2. | Dependent
  3. | Defined of Names.GlobRef.t
val default_tactic : unit Proofview.tactic ref
val add_definition : Names.Id.t -> ?term:Constr.constr -> Constr.types -> UState.t -> ?univdecl:UState.universe_decl -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(Constr.constr -> Constr.constr) -> ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
type fixpoint_kind =
  1. | IsFixpoint of (Names.lident option * Constrexpr.recursion_order_expr) list
  2. | IsCoFixpoint
val add_mutual_definitions : (Names.Id.t * Constr.constr * Constr.types * (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list -> UState.t -> ?univdecl:UState.universe_decl -> ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(Constr.constr -> Constr.constr) -> ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> notations -> fixpoint_kind -> unit
val obligation : (int * Names.Id.t option * Constrexpr.constr_expr option) -> Genarg.glob_generic_argument option -> unit
val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> unit
val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> 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 set_program_mode : bool -> unit
type program_info
val program_tcc_summary_tag : program_info Names.Id.Map.t Summary.Dyn.tag