coq 8.7.2 · OCaml Package

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

val eterm_obligations : 
  Environ.env ->
  Names.Id.t ->
  Evd.evar_map ->
  int ->
  ?status:Evar_kinds.obligation_definition_status ->
  Term.constr ->
  Term.types ->
  (Names.Id.t
   * Term.types
   * Evar_kinds.t Loc.located
   * (bool * Evar_kinds.obligation_definition_status)
   * Int.Set.t
   * unit Proofview.tactic option)
    array
  * ((Term.existential_key * Names.Id.t) list
     * ((Names.Id.t -> Term.constr) ->
     Term.constr ->
     Term.constr))
  * Term.constr
  * Term.types

type obligation_info =
  (Names.Id.t
   * Term.types
   * Evar_kinds.t Loc.located
   * (bool * Evar_kinds.obligation_definition_status)
   * Int.Set.t
   * unit Proofview.tactic option)
    array

type progress =

| Remain of int
| Dependent
| Defined of Globnames.global_reference

val default_tactic : unit Proofview.tactic Pervasives.ref

val add_definition : 
  Names.Id.t ->
  ?term:Term.constr ->
  Term.types ->
  Evd.evar_universe_context ->
  ?pl:Names.Id.t Loc.located list ->
  ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
  ?kind:Decl_kinds.definition_kind ->
  ?tactic:unit Proofview.tactic ->
  ?reduce:(Term.constr -> Term.constr) ->
  ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook ->
  ?opaque:bool ->
  obligation_info ->
  progress

type notations =
  (Vernacexpr.lstring
   * Constrexpr.constr_expr
   * Notation_term.scope_name option)
    list

type fixpoint_kind =

| IsFixpoint of (Names.Id.t Loc.located option * Constrexpr.recursion_order_expr) list
| IsCoFixpoint

val add_mutual_definitions : 
  (Names.Id.t
   * Term.constr
   * Term.types
   * (Constrexpr.explicitation * (bool * bool * bool)) list
   * obligation_info)
    list ->
  Evd.evar_universe_context ->
  ?pl:Names.Id.t Loc.located list ->
  ?tactic:unit Proofview.tactic ->
  ?kind:Decl_kinds.definition_kind ->
  ?reduce:(Term.constr -> Term.constr) ->
  ?hook:(Evd.evar_universe_context -> 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.std_ppcmds

val admit_obligations : Names.Id.t option -> unit

exception NoObligations of Names.Id.t option

val explain_no_obligations : Names.Id.t option -> Pp.std_ppcmds

val set_program_mode : bool -> unit

package coq