Module RetrieveObl
val check_evars : Environ.env -> Evd.evar_map -> unit
type obligation_info
= (Names.Id.t * Constr.types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array
ident, type, location of the original evar, (opaque or transparent, expand or define), dependencies as indexes into the array, tactic to solve it
val retrieve_obligations : Environ.env -> Names.Id.t -> Evd.evar_map -> int -> ?deps:Evar.Set.t -> ?status:Evar_kinds.obligation_definition_status -> EConstr.t -> EConstr.types -> obligation_info * ((Evar.t * Names.Id.t) list * ((Names.Id.t -> EConstr.t) -> EConstr.t -> Constr.t)) * Constr.t * Constr.t
retrieve_obligations env id sigma fs ?status body type
returnsobls, (evnames, evmap), nbody, ntype
a list of obligations built from evars inbody, type
.fs
is the number of function prototypes to try to clear from evars contexts.evnames, evmap
is the list of names / substitution functions used to program with holes. This is not used in Coq, but in the equations plugin;evnames
is actually redundant with the information contained inobls