blob: 13f7b6c1c1051db18cf9533fb28063cdf0c0dc2f (
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
65
66
67
68
69
70
|
(* $Id$ *)
(*i*)
open Pp
open Names
open Term
open Sign
open Environ
open Declare
open Proof_trees
open Tacmach
(*i*)
val proof_prompt : unit -> string
val refining : unit -> bool
val abort_goal : string -> unit
val abort_cur_goal : unit -> unit
val abort_goals : unit -> unit
val abort_refine : ('a -> 'b) -> 'a -> 'b
val msg_proofs : bool -> std_ppcmds
val undo_limit : int ref
val set_undo : int -> unit
val unset_undo : unit -> unit
val undo : int -> unit
val resume_last : unit -> unit
type proof_topstate = {
top_hyps : env * env;
top_goal : goal;
top_strength : strength }
val get_state : unit -> pftreestate * proof_topstate
val get_topstate : unit -> proof_topstate
val get_pftreestate : unit -> pftreestate
val get_evmap_sign : int option -> evar_declarations * env
val set_proof : string option -> unit
val get_proof : unit -> string
val list_proofs : unit -> string list
val add_proof : string * pftreestate * proof_topstate -> unit
val del_proof : string -> unit
val init_proofs : unit -> unit
val mutate : (pftreestate -> pftreestate) -> unit
val rev_mutate : (pftreestate -> pftreestate) -> unit
val start : string * proof_topstate -> unit
val restart : unit -> unit
val proof_prompt : unit -> string
val proof_term : unit -> constr
val start_proof : string -> strength -> Coqast.t -> unit
val start_proof_constr : string -> strength -> constr -> unit
val save_named : bool -> unit
val save_anonymous : bool -> string -> 'a -> unit
val save_anonymous_thm : bool -> string -> unit
val save_anonymous_remark : bool -> string -> unit
val solve_nth : int -> tactic -> unit
val by : tactic -> unit
val traverse : int -> unit
val traverse_nth_goal : int -> unit
val traverse_to : int list -> unit
val make_focus : int -> unit
val focus : unit -> int
val focused_goal : unit -> int
val subtree_solved : unit -> bool
|
