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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
open Pp
open Names
open Term
open Sign
open Environ
open Decl_kinds
open Tacmach
open Tacexpr
(** Several proofs can be opened simultaneously but at most one is
focused at some time. The following functions work by side-effect
on current set of open proofs. In this module, ``proofs'' means an
open proof (something started by vernacular command [Goal], [Lemma]
or [Theorem]), and ``goal'' means a subgoal of the current focused
proof *)
(** {6 ... } *)
(** [refining ()] tells if there is some proof in progress, even if a not
focused one *)
val refining : unit -> bool
(** [check_no_pending_proofs ()] fails if there is still some proof in
progress *)
val check_no_pending_proofs : unit -> unit
(** {6 ... } *)
(** [delete_proof name] deletes proof of name [name] or fails if no proof
has this name *)
val delete_proof : identifier located -> unit
(** [delete_current_proof ()] deletes current focused proof or fails if
no proof is focused *)
val delete_current_proof : unit -> unit
(** [delete_all_proofs ()] deletes all open proofs if any *)
val delete_all_proofs : unit -> unit
(** {6 ... } *)
(** [undo n] undoes the effect of the last [n] tactics applied to the
current proof; it fails if no proof is focused or if the ``undo''
stack is exhausted *)
val undo : int -> unit
(** [undo_todepth n] resets the proof to its nth step (does [undo (d-n)] where d
is the depth of the undo stack). *)
val undo_todepth : int -> unit
(** Returns the depth of the current focused proof stack, this is used
to put informations in coq prompt (in emacs mode). *)
val current_proof_depth: unit -> int
(** {6 ... } *)
(** [start_proof s str env t hook tac] starts a proof of name [s] and
conclusion [t]; [hook] is optionally a function to be applied at
proof end (e.g. to declare the built constructions as a coercion
or a setoid morphism); init_tac is possibly a tactic to
systematically apply at initialization time (e.g. to start the
proof of mutually dependent theorems) *)
type lemma_possible_guards = Proof_global.lemma_possible_guards
val start_proof :
identifier -> goal_kind -> named_context_val -> constr ->
?init_tac:tactic -> ?compute_guard:lemma_possible_guards ->
declaration_hook -> unit
(** [restart_proof ()] restarts the current focused proof from the beginning
or fails if no proof is focused *)
val restart_proof : unit -> unit
(** {6 ... } *)
(** [cook_proof opacity] turns the current proof (assumed completed) into
a constant with its name, kind and possible hook (see [start_proof]);
it fails if there is no current proof of if it is not completed;
it also tells if the guardness condition has to be inferred. *)
val cook_proof : (Proof.proof -> unit) ->
identifier *
(Entries.definition_entry * lemma_possible_guards * goal_kind *
declaration_hook)
(** To export completed proofs to xml *)
val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit
(** {6 ... } *)
(** [get_Proof.proof ()] returns the current focused pending proof or
raises [UserError "no focused proof"] *)
val get_pftreestate : unit -> Proof.proof
(** [get_goal_context n] returns the context of the [n]th subgoal of
the current focused proof or raises a [UserError] if there is no
focused proof or if there is no more subgoals *)
val get_goal_context : int -> Evd.evar_map * env
(** [get_current_goal_context ()] works as [get_goal_context 1] *)
val get_current_goal_context : unit -> Evd.evar_map * env
(** [current_proof_statement] *)
val current_proof_statement :
unit -> identifier * goal_kind * types * declaration_hook
(** {6 ... } *)
(** [get_current_proof_name ()] return the name of the current focused
proof or failed if no proof is focused *)
val get_current_proof_name : unit -> identifier
(** [get_all_proof_names ()] returns the list of all pending proof names.
The first name is the current proof, the other names may come in
any order. *)
val get_all_proof_names : unit -> identifier list
(** {6 ... } *)
(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
by [solve_nth] *)
val set_end_tac : tactic -> unit
(** {6 ... } *)
(** [set_used_variables l] declares that section variables [l] will be
used in the proof *)
val set_used_variables : identifier list -> unit
val get_used_variables : unit -> Sign.section_context option
(** {6 ... } *)
(** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
current focused proof or raises a UserError if no proof is focused or
if there is no [n]th subgoal *)
val solve_nth : ?with_end_tac:bool -> int -> tactic -> unit
(** [by tac] applies tactic [tac] to the 1st subgoal of the current
focused proof or raises a UserError if there is no focused proof or
if there is no more subgoals *)
val by : tactic -> unit
(** [instantiate_nth_evar_com n c] instantiate the [n]th undefined
existential variable of the current focused proof by [c] or raises a
UserError if no proof is focused or if there is no such [n]th
existential variable *)
val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit
(** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic ->
Entries.definition_entry
val build_by_tactic : env -> types -> tactic -> constr
(** Declare the default tactic to fill implicit arguments *)
val declare_implicit_tactic : tactic -> unit
(* Raise Exit if cannot solve *)
val solve_by_implicit_tactic : env -> Evd.evar_map -> existential -> constr
|
