diff options
author | 2007-08-18 20:34:57 +0000 | |
---|---|---|
committer | 2007-08-18 20:34:57 +0000 | |
commit | be2a2fda89bba47d5342b7aebc10efd97f1d68b9 (patch) | |
tree | 45a70ccd12dc139a53b49daba9c9821ffe2fd035 /contrib/subtac/subtac_obligations.mli | |
parent | 763b05d3e66a0c0c49bad97434d891d22c1054dc (diff) | |
parent | 72b9a7df489ea47b3e5470741fd39f6100d31676 (diff) |
Merge commit 'upstream/8.1.pl1+dfsg'
Diffstat (limited to 'contrib/subtac/subtac_obligations.mli')
-rw-r--r-- | contrib/subtac/subtac_obligations.mli | 20 |
1 files changed, 17 insertions, 3 deletions
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 3981d4c6..f015b80b 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -1,8 +1,10 @@ open Util -type obligation_info = (Names.identifier * Term.types * Intset.t) array +type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array + (* ident, type, opaque or transparent, dependencies *) -val set_default_tactic : Proof_type.tactic -> unit +val set_default_tactic : Tacexpr.glob_tactic_expr -> unit +val default_tactic : unit -> Proof_type.tactic val add_definition : Names.identifier -> Term.constr -> Term.types -> obligation_info -> unit @@ -14,8 +16,20 @@ 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 -> unit +val solve_obligations : Names.identifier option -> Proof_type.tactic -> int +(* Number of remaining obligations to be solved for this program *) + +val solve_all_obligations : Proof_type.tactic -> unit + +val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic -> unit + +val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit val show_obligations : Names.identifier option -> unit val admit_obligations : Names.identifier option -> unit + +exception NoObligations of Names.identifier option + +val explain_no_obligations : Names.identifier option -> Pp.std_ppcmds + |