diff options
| -rw-r--r-- | vernac/obligations.mli | 44 |
1 files changed, 25 insertions, 19 deletions
diff --git a/vernac/obligations.mli b/vernac/obligations.mli index f97bc784c3..3bffdb5f52 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -18,27 +18,33 @@ val check_evars : env -> evar_map -> unit val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list -(* env, id, evars, number of function prototypes to try to clear from - evars contexts, object and type *) -val eterm_obligations : env -> Id.t -> evar_map -> int -> - ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types -> - (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * - unit Proofview.tactic option) array - (* Existential key, obl. name, type as product, - location of the original evar, associated tactic, - status and dependencies as indexes into the array *) - * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * - constr * types - (* Translations from existential identifiers to obligation identifiers - and for terms with existentials to closed terms, given a - translation from obligation identifiers to constrs, new term, new type *) - +(* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) type obligation_info = (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array - (* ident, type, location, (opaque or transparent, expand or define), - dependencies, tactic to solve it *) + (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array + +(* env, id, evars, number of function prototypes to try to clear from + evars contexts, object and type *) +val eterm_obligations + : env + -> Id.t + -> evar_map + -> int + -> ?status:Evar_kinds.obligation_definition_status + -> EConstr.constr + -> EConstr.types + -> obligation_info * + + (* Existential key, obl. name, type as product, location of the + original evar, associated tactic, status and dependencies as + indexes into the array *) + ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * + + (* Translations from existential identifiers to obligation + identifiers and for terms with existentials to closed terms, + given a translation from obligation identifiers to constrs, + new term, new type *) + constr * types val default_tactic : unit Proofview.tactic ref |