Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg

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
+