Obls (coq-core.Declare.Obls)

type fixpoint_kind =

| IsFixpoint of Names.lident option list

| IsCoFixpoint

val check_solved_obligations : pm:OblState.t -> what_for:Pp.t -> unit

Check obligations are properly solved before closing the what_for section / module

val default_tactic : unit Proofview.tactic Stdlib.ref

type progress =

`\| Remain of int`	(* n obligations remaining *)
`\| Dependent`	(* Dependent on other definitions *)
`\| Defined of Names.GlobRef.t`	(* Defined as id *)

Resolution status of a program

val prepare_obligation : 
  name:Names.Id.t ->
  types:EConstr.t option ->
  body:EConstr.t ->
  Evd.evar_map ->
  Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info

Prepare API, to be removed once we provide the corresponding 1-step API

val add_definition : 
  pm:OblState.t ->
  cinfo:Constr.types CInfo.t ->
  info:Info.t ->
  ?obl_hook:OblState.t Hook.g ->
  ?term:Constr.t ->
  uctx:UState.t ->
  ?tactic:unit Proofview.tactic ->
  ?reduce:( Constr.t -> Constr.t ) ->
  ?opaque:bool ->
  RetrieveObl.obligation_info ->
  OblState.t * progress

Start a Program Definition c proof. uctx udecl impargs kind scope poly etc... come from the interpretation of the vernacular; `obligation_info` was generated by RetrieveObl It will return whether all the obligations were solved; if so, it will also register c with the kernel.

val add_mutual_definitions : 
  (Constr.t CInfo.t * Constr.t * RetrieveObl.obligation_info) list ->
  pm:OblState.t ->
  info:Info.t ->
  ?obl_hook:OblState.t Hook.g ->
  uctx:UState.t ->
  ?tactic:unit Proofview.tactic ->
  ?reduce:( Constr.t -> Constr.t ) ->
  ?opaque:bool ->
  ntns:Metasyntax.notation_interpretation_decl list ->
  fixpoint_kind ->
  OblState.t

Start a Program Fixpoint declaration, similar to the above, except it takes a list now.

val obligation : 
  (int * Names.Id.t option * Constrexpr.constr_expr option) ->
  pm:OblState.t ->
  Genarg.glob_generic_argument option ->
  Proof.t

Implementation of the Obligation command

val next_obligation : 
  pm:OblState.t ->
  ?final:bool ->
  Names.Id.t option ->
  Genarg.glob_generic_argument option ->
  Proof.t

Implementation of the Next Obligation and Final Obligation commands

val solve_obligations : 
  pm:OblState.t ->
  Names.Id.t option ->
  unit Proofview.tactic option ->
  OblState.t * progress

Implementation of the Solve Obligation command

val solve_all_obligations : 
  pm:OblState.t ->
  unit Proofview.tactic option ->
  OblState.t

val try_solve_obligations : 
  pm:OblState.t ->
  Names.Id.t option ->
  unit Proofview.tactic option ->
  OblState.t

val show_obligations : pm:OblState.t -> ?msg:bool -> Names.Id.t option -> unit

val show_term : pm:OblState.t -> Names.Id.t option -> Pp.t

val admit_obligations : pm:OblState.t -> Names.Id.t option -> OblState.t

val check_program_libraries : unit -> unit