diff options
Diffstat (limited to 'contrib/subtac/subtac_obligations.mli')
| -rw-r--r-- | contrib/subtac/subtac_obligations.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 07f151697a..972aadce6d 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -2,6 +2,8 @@ open Util type obligation_info = (Names.identifier * Term.types * Intset.t) array +val set_default_tactic : Proof_type.tactic -> unit + val add_definition : Names.identifier -> Term.constr -> Term.types -> obligation_info -> unit @@ -13,3 +15,5 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op val solve_obligations : Names.identifier option -> Proof_type.tactic -> unit val show_obligations : Names.identifier option -> unit + +val admit_obligations : Names.identifier option -> unit |