8
(identifier * Term.types * loc *
9
obligation_definition_status * Intset.t * Tacexpr.raw_tactic_expr option) array
10
(* ident, type, location, (opaque or transparent, expand or define),
11
dependencies, tactic to solve it *)
13
type progress = (* Resolution status of a program *)
14
| Remain of int (* n obligations remaining *)
15
| Dependent (* Dependent on other definitions *)
16
| Defined of global_reference (* Defined as id *)
18
val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
19
val default_tactic : unit -> Proof_type.tactic
21
val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
22
val get_proofs_transparency : unit -> bool
24
val add_definition : Names.identifier -> Term.constr -> Term.types ->
25
?implicits:(Topconstr.explicitation * (bool * bool)) list ->
26
?kind:Decl_kinds.definition_kind ->
27
?tactic:Proof_type.tactic ->
28
?hook:Tacexpr.declaration_hook -> obligation_info -> progress
30
type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
32
val add_mutual_definitions :
33
(Names.identifier * Term.constr * Term.types *
34
(Topconstr.explicitation * (bool * bool)) list * obligation_info) list ->
35
?tactic:Proof_type.tactic ->
36
?kind:Decl_kinds.definition_kind ->
37
?hook:Tacexpr.declaration_hook ->
39
Command.fixpoint_kind -> unit
41
val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
43
val next_obligation : Names.identifier option -> unit
45
val solve_obligations : Names.identifier option -> Proof_type.tactic option -> progress
46
(* Number of remaining obligations to be solved for this program *)
48
val solve_all_obligations : Proof_type.tactic option -> unit
50
val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic option -> unit
52
val try_solve_obligations : Names.identifier option -> Proof_type.tactic option -> unit
54
val show_obligations : ?msg:bool -> Names.identifier option -> unit
56
val show_term : Names.identifier option -> unit
58
val admit_obligations : Names.identifier option -> unit
60
exception NoObligations of Names.identifier option
62
val explain_no_obligations : Names.identifier option -> Pp.std_ppcmds