diff options
Diffstat (limited to 'contrib/subtac/subtac_obligations.mli')
| -rw-r--r-- | contrib/subtac/subtac_obligations.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 0ad9e730d5..8a64551369 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -17,7 +17,10 @@ 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 -> int - (* Number of remaining obligations to be solved for this program *) +(* Number of remaining obligations to be solved for this program *) + +val solve_all_obligations : Proof_type.tactic -> unit + val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit val show_obligations : Names.identifier option -> unit |