← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to proofs/pfedit.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
proofs/pfedit.mli
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: pfedit.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
 
10
 
 
11
(*i*)
 
12
open Util
 
13
open Pp
 
14
open Names
 
15
open Term
 
16
open Sign
 
17
open Environ
 
18
open Decl_kinds
 
19
open Tacmach
 
20
open Tacexpr
 
21
(*i*)
 
22
 
 
23
(*s Several proofs can be opened simultaneously but at most one is
 
24
   focused at some time. The following functions work by side-effect
 
25
   on current set of open proofs. In this module, ``proofs'' means an
 
26
   open proof (something started by vernacular command [Goal], [Lemma]
 
27
   or [Theorem]), and ``goal'' means a subgoal of the current focused
 
28
   proof *)
 
29
 
 
30
(*s [refining ()] tells if there is some proof in progress, even if a not
 
31
   focused one *)
 
32
 
 
33
val refining : unit -> bool
 
34
 
 
35
(* [check_no_pending_proofs ()] fails if there is still some proof in
 
36
   progress *)
 
37
 
 
38
val check_no_pending_proofs : unit -> unit
 
39
 
 
40
(*s [delete_proof name] deletes proof of name [name] or fails if no proof
 
41
    has this name *)
 
42
 
 
43
val delete_proof : identifier located -> unit
 
44
 
 
45
(* [delete_current_proof ()] deletes current focused proof or fails if
 
46
    no proof is focused *)
 
47
 
 
48
val delete_current_proof : unit -> unit
 
49
 
 
50
(* [delete_all_proofs ()] deletes all open proofs if any *)
 
51
 
 
52
val delete_all_proofs : unit -> unit
 
53
 
 
54
(*s [undo n] undoes the effect of the last [n] tactics applied to the
 
55
    current proof; it fails if no proof is focused or if the ``undo''
 
56
    stack is exhausted *)
 
57
 
 
58
val undo : int -> unit
 
59
 
 
60
(* Same as undo, but undoes the current proof stack to reach depth
 
61
   [n]. This is used in [vernac_backtrack]. *)
 
62
val undo_todepth : int -> unit
 
63
 
 
64
(* Returns the depth of the current focused proof stack, this is used
 
65
   to put informations in coq prompt (in emacs mode). *)
 
66
val current_proof_depth: unit -> int
 
67
 
 
68
(* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None]
 
69
   sets the size to the default value (12) *)
 
70
 
 
71
val set_undo : int option -> unit
 
72
val get_undo : unit -> int option
 
73
 
 
74
(*s [start_proof s str env t hook tac] starts a proof of name [s] and
 
75
    conclusion [t]; [hook] is optionally a function to be applied at
 
76
    proof end (e.g. to declare the built constructions as a coercion
 
77
    or a setoid morphism); init_tac is possibly a tactic to
 
78
    systematically apply at initialization time (e.g. to start the
 
79
    proof of mutually dependent theorems) *)
 
80
 
 
81
val start_proof : 
 
82
  identifier -> goal_kind -> named_context_val -> constr ->
 
83
    ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
 
84
 
 
85
(* [restart_proof ()] restarts the current focused proof from the beginning
 
86
   or fails if no proof is focused *)
 
87
 
 
88
val restart_proof : unit -> unit
 
89
 
 
90
(*s [resume_last_proof ()] focus on the last unfocused proof or fails
 
91
   if there is no suspended proofs *)
 
92
 
 
93
val resume_last_proof : unit -> unit
 
94
 
 
95
(* [resume_proof name] focuses on the proof of name [name] or
 
96
   raises [UserError] if no proof has name [name] *)
 
97
 
 
98
val resume_proof : identifier located -> unit
 
99
 
 
100
(* [suspend_proof ()] unfocuses the current focused proof or
 
101
   failed with [UserError] if no proof is currently focused *)
 
102
 
 
103
val suspend_proof : unit -> unit
 
104
 
 
105
(*s [cook_proof opacity] turns the current proof (assumed completed) into
 
106
    a constant with its name, kind and possible hook (see [start_proof]);
 
107
    it fails if there is no current proof of if it is not completed;
 
108
    it also tells if the guardness condition has to be inferred. *)
 
109
 
 
110
val cook_proof : (Refiner.pftreestate -> unit) -> 
 
111
  identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook)
 
112
 
 
113
(* To export completed proofs to xml *)
 
114
val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit
 
115
 
 
116
(*s [get_pftreestate ()] returns the current focused pending proof or
 
117
   raises [UserError "no focused proof"] *)
 
118
 
 
119
val get_pftreestate : unit -> pftreestate
 
120
 
 
121
(* [get_end_tac ()] returns the current tactic to apply to all new subgoal *)
 
122
 
 
123
val get_end_tac : unit -> tactic option
 
124
 
 
125
(* [get_goal_context n] returns the context of the [n]th subgoal of
 
126
   the current focused proof or raises a [UserError] if there is no
 
127
   focused proof or if there is no more subgoals *)
 
128
 
 
129
val get_goal_context : int -> Evd.evar_map * env
 
130
 
 
131
(* [get_current_goal_context ()] works as [get_goal_context 1] *)
 
132
 
 
133
val get_current_goal_context : unit -> Evd.evar_map * env
 
134
 
 
135
(* [current_proof_statement] *)
 
136
 
 
137
val current_proof_statement :
 
138
  unit -> identifier * goal_kind * types * declaration_hook
 
139
 
 
140
(*s [get_current_proof_name ()] return the name of the current focused
 
141
    proof or failed if no proof is focused *)
 
142
 
 
143
val get_current_proof_name : unit -> identifier
 
144
 
 
145
(* [get_all_proof_names ()] returns the list of all pending proof names *)
 
146
 
 
147
val get_all_proof_names : unit -> identifier list
 
148
 
 
149
(*s [set_end_tac tac] applies tactic [tac] to all subgoal generate
 
150
    by [solve_nth] *)
 
151
 
 
152
val set_end_tac : tactic -> unit
 
153
 
 
154
(*s [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the
 
155
   current focused proof or raises a UserError if no proof is focused or
 
156
   if there is no [n]th subgoal *)
 
157
 
 
158
val solve_nth : int -> tactic -> unit
 
159
 
 
160
(* [by tac] applies tactic [tac] to the 1st subgoal of the current
 
161
   focused proof or raises a UserError if there is no focused proof or
 
162
   if there is no more subgoals *)
 
163
 
 
164
val by : tactic -> unit
 
165
 
 
166
(* [instantiate_nth_evar_com n c] instantiate the [n]th undefined
 
167
   existential variable of the current focused proof by [c] or raises a
 
168
   UserError if no proof is focused or if there is no such [n]th
 
169
   existential variable *)
 
170
 
 
171
val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit
 
172
 
 
173
(*s To deal with subgoal focus *)
 
174
 
 
175
val make_focus : int -> unit
 
176
val focus : unit -> int
 
177
val focused_goal : unit -> int
 
178
val subtree_solved : unit -> bool
 
179
val tree_solved : unit -> bool
 
180
val top_tree_solved : unit -> bool
 
181
 
 
182
val reset_top_of_tree : unit -> unit
 
183
val reset_top_of_script : unit -> unit
 
184
 
 
185
val traverse : int -> unit
 
186
val traverse_nth_goal : int -> unit
 
187
val traverse_next_unproven : unit -> unit
 
188
val traverse_prev_unproven : unit -> unit
 
189
 
 
190
 
 
191
(* These two functions make it possible to implement more elaborate
 
192
   proof and goal management, as it is done, for instance in pcoq *)
 
193
val traverse_to : int list -> unit
 
194
val mutate : (pftreestate -> pftreestate) -> unit