diff options
Diffstat (limited to 'contrib/subtac/subtac_obligations.mli')
| -rw-r--r-- | contrib/subtac/subtac_obligations.mli | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 6d13e3bd..60c0a413 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,9 +1,14 @@ open Names open Util open Libnames +open Evd +open Proof_type -type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array - (* ident, type, location, opaque or transparent, dependencies *) +type obligation_info = + (identifier * Term.types * loc * + obligation_definition_status * Intset.t * Tacexpr.raw_tactic_expr option) array + (* ident, type, location, (opaque or transparent, expand or define), + dependencies, tactic to solve it *) type progress = (* Resolution status of a program *) | Remain of int (* n obligations remaining *) @@ -21,6 +26,7 @@ type definition_hook = global_reference -> unit val add_definition : Names.identifier -> Term.constr -> Term.types -> ?implicits:(Topconstr.explicitation * (bool * bool)) list -> ?kind:Decl_kinds.definition_kind -> + ?tactic:Proof_type.tactic -> ?hook:definition_hook -> obligation_info -> progress type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list @@ -28,6 +34,7 @@ type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) val add_mutual_definitions : (Names.identifier * Term.constr * Term.types * (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> + ?tactic:Proof_type.tactic -> ?kind:Decl_kinds.definition_kind -> notations -> Command.fixpoint_kind -> unit @@ -36,14 +43,14 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op val next_obligation : Names.identifier option -> unit -val solve_obligations : Names.identifier option -> Proof_type.tactic -> progress +val solve_obligations : Names.identifier option -> Proof_type.tactic option -> progress (* Number of remaining obligations to be solved for this program *) -val solve_all_obligations : Proof_type.tactic -> unit +val solve_all_obligations : Proof_type.tactic option -> unit -val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic -> unit +val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic option -> unit -val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit +val try_solve_obligations : Names.identifier option -> Proof_type.tactic option -> unit val show_obligations : ?msg:bool -> Names.identifier option -> unit |