diff options
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index e95881ba..8c0c7f55 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,7 +6,7 @@ (* * 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 $Id: pfedit.mli 9154 2006-09-20 17:18:18Z corbinea $ i*) (*i*) open Util @@ -57,6 +57,14 @@ val delete_all_proofs : unit -> unit val undo : int -> unit +(* Same as undo, but undoes the current proof stack to reach depth + [n]. This is used in [vernac_backtrack]. *) +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 + (* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None] sets the size to the default value (12) *) @@ -68,7 +76,7 @@ val get_undo : unit -> int option declare the built constructions as a coercion or a setoid morphism) *) val start_proof : - identifier -> goal_kind -> named_context -> constr + identifier -> goal_kind -> named_context_val -> constr -> declaration_hook -> unit (* [restart_proof ()] restarts the current focused proof from the beginning @@ -164,8 +172,12 @@ val make_focus : int -> unit val focus : unit -> int val focused_goal : unit -> int val subtree_solved : unit -> bool +val tree_solved : unit -> bool +val top_tree_solved : unit -> bool val reset_top_of_tree : unit -> unit +val reset_top_of_script : unit -> unit + val traverse : int -> unit val traverse_nth_goal : int -> unit val traverse_next_unproven : unit -> unit @@ -176,8 +188,3 @@ val traverse_prev_unproven : unit -> unit 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 |