Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 12 insertions, 28 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index a1bea931..5cf66d36 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coq.mli 11126 2008-06-13 18:45:04Z herbelin $ i*)
+(*i $Id$ i*)
 
 open Names
 open Term
@@ -29,31 +29,19 @@ type printing_state = {
 
 val printing_state : printing_state
 
-type reset_mark =
-  | ResetToId of Names.identifier
-  | ResetToState of Libnames.object_name
+type reset_info
 
-type reset_status =
-  | NoReset
-  | ResetAtSegmentStart of Names.identifier
-  | ResetAtRegisteredObject of reset_mark
-
-type undo_info = identifier list
-
-val undo_info : unit -> undo_info
-
-type reset_info = reset_status * undo_info * bool ref
-
-val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
 val reset_initial : unit -> unit
-val reset_to : reset_mark -> unit
-val reset_to_mod : identifier -> unit
 
-val init : unit -> string list 
-val interp : bool -> string -> reset_info * (Util.loc * Vernacexpr.vernac_expr)
+val init : unit -> string list
+val interp : bool -> string -> reset_info
 val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
-val interp_and_replace : string -> 
-      (reset_info * (Util.loc * Vernacexpr.vernac_expr)) * string
+val interp_and_replace : string ->
+      reset_info * string
+
+val push_phrase : ('a * reset_info) Stack.t -> reset_info -> 'a -> unit
+
+val rewind : reset_info list -> ('a * reset_info) Stack.t -> unit
 
 val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool
 val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool
@@ -62,7 +50,7 @@ val is_vernac_proof_ending_command : Vernacexpr.vernac_expr -> bool
 
 (* type hyp = (identifier * constr option * constr) * string *)
 
-type hyp = env * evar_map * 
+type hyp = env * evar_map *
            ((identifier*string) * constr option * constr) * (string * string)
 type meta = env * evar_map * string
 type concl = env * evar_map * constr * string
@@ -72,8 +60,6 @@ val get_current_goals : unit -> goal list
 
 val get_current_pm_goal : unit -> goal
 
-val get_current_goals_nb : unit -> int
-
 val print_no_goal : unit -> string
 
 val process_exn : exn -> string*(Util.loc option)
@@ -88,13 +74,11 @@ val is_in_loadpath : string -> bool
 val make_cases : string -> string list list
 
 
-type tried_tactic = 
+type tried_tactic =
   | Interrupted
   | Success of int (* nb of goals after *)
   | Failed
 
-val try_interptac: string -> tried_tactic
-
 (* Message to display in lower status bar. *)
 
 val current_status : unit -> string