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 178 179 180 181 182 183

(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRSEcole PolytechniqueINRIA FutursUniversite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: pfedit.mli,v 1.35.2.1 2004/07/16 19:30:49 herbelin Exp $ i*)
(*i*)
open Util
open Pp
open Names
open Term
open Sign
open Environ
open Decl_kinds
open Tacmach
open Tacexpr
(*i*)
(*s Several proofs can be opened simultaneously but at most one is
focused at some time. The following functions work by sideeffect
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 *)
(*s [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
(*s [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
(*s [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
(* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None]
sets the size to the default value (12) *)
val set_undo : int option > unit
val get_undo : unit > int option
(*s [start_proof s str env t hook] 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) *)
val start_proof :
identifier > goal_kind > named_context > constr
> 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
(*s [resume_last_proof ()] focus on the last unfocused proof or fails
if there is no suspended proofs *)
val resume_last_proof : unit > unit
(* [resume_proof name] focuses on the proof of name [name] or
raises [UserError] if no proof has name [name] *)
val resume_proof : identifier located > unit
(* [suspend_proof ()] unfocuses the current focused proof or
failed with [UserError] if no proof is currently focused *)
val suspend_proof : unit > unit
(*s [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 *)
val cook_proof : unit >
identifier * (Entries.definition_entry * goal_kind * declaration_hook)
(* To export completed proofs to xml *)
val set_xml_cook_proof : (goal_kind * pftreestate > unit) > unit
(*s [get_pftreestate ()] returns the current focused pending proof or
raises [UserError "no focused proof"] *)
val get_pftreestate : unit > pftreestate
(* [get_end_tac ()] returns the current tactic to apply to all new subgoal *)
val get_end_tac : unit > tactic option
(* [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
(*s [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 *)
val get_all_proof_names : unit > identifier list
(*s [set_end_tac tac] applies tactic [tac] to all subgoal generate
by [solve_nth] *)
val set_end_tac : tactic > unit
(*s [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 : 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
(*s To deal with subgoal focus *)
val make_focus : int > unit
val focus : unit > int
val focused_goal : unit > int
val subtree_solved : unit > bool
val reset_top_of_tree : unit > unit
val traverse : int > unit
val traverse_nth_goal : int > unit
val traverse_next_unproven : unit > unit
val traverse_prev_unproven : unit > unit
(* These two functions make it possible to implement more elaborate
proof and goal management, as it is done, for instance in pcoq *)
val traverse_to : int list > unit
val mutate : (pftreestate > pftreestate) > unit
(** Printers *)
val pr_open_subgoals : unit > std_ppcmds
val pr_nth_open_subgoal : int > std_ppcmds
