From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 toplevel/backtrack.mli | 99 --------------------------------------------------
 1 file changed, 99 deletions(-)
 delete mode 100644 toplevel/backtrack.mli

(limited to 'toplevel/backtrack.mli')

diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli
deleted file mode 100644
index 315575dc..00000000
--- a/toplevel/backtrack.mli
+++ /dev/null
@@ -1,99 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(** Command history stack
-
-    We maintain a stack of the past states of the system after each
-    (non-state-preserving) interpreted commands
-*)
-
-(** [mark_command ast] marks the end of a command:
-    - it stores a frozen state and a end of command in the Lib stack,
-    - it stores the current state information in the command history
-    stack *)
-
-val mark_command : Vernacexpr.vernac_expr -> unit
-
-(** Is this history stack active (i.e. nonempty) ?
-    The stack is currently inactive when compiling files (coqc). *)
-
-val is_active : unit -> bool
-
-(** The [Invalid] exception is raised when one of the following function
-    tries to empty the history stack, or reach an unknown states, etc.
-    The stack is preserved in these cases. *)
-
-exception Invalid
-
-(** Nota Bene: it is critical for the following functions that proofs
-    are nested in a regular way (i.e. no more Resume or Suspend commands
-    as earlier). *)
-
-(** Backtracking by a certain number of (non-state-preserving) commands.
-    This is used by Coqide.
-    It may actually undo more commands than asked : for instance instead
-    of jumping back in the middle of a finished proof, we jump back before
-    this proof. The number of extra backtracked command is returned at
-    the end. *)
-
-val back : int -> int
-
-(** Backtracking to a certain state number, and reset proofs accordingly.
-    We may end on some earlier state if needed to avoid re-opening proofs.
-    Return the state number on which we finally end. *)
-
-val backto : int -> int
-
-(** Old [Backtrack] code with corresponding update of the history stack.
-    [Backtrack] is now deprecated (in favor of [BackTo]) but is kept for
-    compatibility with ProofGeneral. It's completely up to ProofGeneral
-    to decide where to go and how to adapt proofs. Note that the choices
-    of ProofGeneral are currently not always perfect (for instance when
-    backtracking an Undo). *)
-
-val backtrack : int -> int -> int -> unit
-
-(** [reset_initial] resets the system and clears the command history
-    stack, only pushing back the initial entry. It should be equivalent
-    to [backto Lib.first_command_label], but sligthly more efficient. *)
-
-val reset_initial : unit -> unit
-
-(** Reset to the last known state just before defining [id] *)
-
-val reset_name : Names.identifier Util.located -> unit
-
-(** When a proof is ended (via either Qed/Admitted/Restart/Abort),
-    old proof steps should be marked differently to avoid jumping back
-    to them:
-     - either this proof isn't there anymore in the proof engine
-     - either a proof with the same name is there, but it's a more recent
-       attempt after a Restart/Abort, we shouldn't mix the two.
-    We also mark as unreachable the proof steps cancelled via a Undo.
-*)
-
-val mark_unreachable : ?after:int -> Names.identifier list -> unit
-
-(** Parse the history stack for printing the script of a proof *)
-
-val get_script : Names.identifier -> (Vernacexpr.vernac_expr * int) list
-
-
-(** For debug purpose, a dump of the history *)
-
-type info = {
-  label : int;
-  nproofs : int;
-  prfname : Names.identifier option;
-  prfdepth : int;
-  ngoals : int;
-  cmd : Vernacexpr.vernac_expr;
-  mutable reachable : bool;
-}
-
-val dump_history : unit -> info list
-- 
cgit v1.2.3