package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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

retrieve_obligations env id sigma fs ?status body type returns obls, (evnames, evmap), nbody, ntype a list of obligations built from evars in body, 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 in [obls]

OCaml

Innovation. Community. Security.