diff options
Diffstat (limited to 'toplevel/obligations.mli')
| -rw-r--r-- | toplevel/obligations.mli | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index b2320a57..69d20696 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -33,7 +33,8 @@ val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar evars contexts, object and type *) val eterm_obligations : env -> Id.t -> evar_map -> int -> ?status:Evar_kinds.obligation_definition_status -> constr -> types -> - (Id.t * types * Evar_kinds.t Loc.located * Evar_kinds.obligation_definition_status * Int.Set.t * + (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, @@ -46,7 +47,7 @@ val eterm_obligations : env -> Id.t -> evar_map -> int -> type obligation_info = (Id.t * Term.types * Evar_kinds.t Loc.located * - Evar_kinds.obligation_definition_status * Int.Set.t * unit Proofview.tactic option) array + (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 *) @@ -54,16 +55,12 @@ type progress = (* Resolution status of a program *) | Remain of int (* n obligations remaining *) | Dependent (* Dependent on other definitions *) | Defined of global_reference (* Defined as id *) - -val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit -val get_default_tactic : unit -> locality_flag * unit Proofview.tactic -val print_default_tactic : unit -> Pp.std_ppcmds -val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *) -val get_proofs_transparency : unit -> bool +val default_tactic : unit Proofview.tactic ref val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> Evd.evar_universe_context -> + ?pl:(Id.t Loc.located list) -> (* Universe binders *) ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> @@ -81,6 +78,7 @@ 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:(Id.t Loc.located list) -> (* Universe binders *) ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(Term.constr -> Term.constr) -> |