blob: 60c0a4139a42653b90ec446461c02d2a850eee6b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
open Names
open Util
open Libnames
open Evd
open Proof_type
type obligation_info =
(identifier * Term.types * loc *
obligation_definition_status * Intset.t * Tacexpr.raw_tactic_expr 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 : Tacexpr.glob_tactic_expr -> unit
val default_tactic : unit -> Proof_type.tactic
val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
val get_proofs_transparency : unit -> bool
type definition_hook = global_reference -> unit
val add_definition : Names.identifier -> Term.constr -> Term.types ->
?implicits:(Topconstr.explicitation * (bool * bool)) list ->
?kind:Decl_kinds.definition_kind ->
?tactic:Proof_type.tactic ->
?hook:definition_hook -> obligation_info -> progress
type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
val add_mutual_definitions :
(Names.identifier * Term.constr * Term.types *
(Topconstr.explicitation * (bool * bool)) list * obligation_info) list ->
?tactic:Proof_type.tactic ->
?kind:Decl_kinds.definition_kind ->
notations ->
Command.fixpoint_kind -> unit
val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
val next_obligation : Names.identifier 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
|
