diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /plugins/subtac/subtac_obligations.mli | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'plugins/subtac/subtac_obligations.mli')
-rw-r--r-- | plugins/subtac/subtac_obligations.mli | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli new file mode 100644 index 00000000..1608c134 --- /dev/null +++ b/plugins/subtac/subtac_obligations.mli @@ -0,0 +1,69 @@ +open Names +open Util +open Libnames +open Evd +open Proof_type + +type obligation_info = + (identifier * Term.types * loc * + obligation_definition_status * Intset.t * tactic 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 *) + | Dependent (* Dependent on other definitions *) + | Defined of global_reference (* Defined as id *) + +val set_default_tactic : bool -> Tacexpr.glob_tactic_expr -> unit +val default_tactic : unit -> Proof_type.tactic +val default_tactic_expr : unit -> Tacexpr.glob_tactic_expr + +val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *) +val get_proofs_transparency : unit -> bool + +val add_definition : Names.identifier -> ?term:Term.constr -> Term.types -> + ?implicits:(Topconstr.explicitation * (bool * bool * bool)) list -> + ?kind:Decl_kinds.definition_kind -> + ?tactic:Proof_type.tactic -> + ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress + +type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list + +type fixpoint_kind = + | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list + | IsCoFixpoint + +val add_mutual_definitions : + (Names.identifier * Term.constr * Term.types * + (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list -> + ?tactic:Proof_type.tactic -> + ?kind:Decl_kinds.definition_kind -> + ?hook:Tacexpr.declaration_hook -> + notations -> + fixpoint_kind -> unit + +val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> + Tacexpr.raw_tactic_expr option -> unit + +val next_obligation : Names.identifier option -> Tacexpr.raw_tactic_expr option -> unit + +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 option -> unit + +val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic option -> unit + +val try_solve_obligations : Names.identifier option -> Proof_type.tactic option -> unit + +val show_obligations : ?msg:bool -> Names.identifier option -> unit + +val show_term : 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 + |