Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 43 insertions, 13 deletions

diff --git a/ide/coq.mli b/ide/coq.mli
index 4b4c3267..a1bea931 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -6,22 +6,59 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coq.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
+(*i $Id: coq.mli 11126 2008-06-13 18:45:04Z herbelin $ i*)
 
 open Names
 open Term
 open Environ
 open Evd
 
+val short_version : unit -> string
 val version : unit -> string
 
+type printing_state = {
+  mutable printing_implicit : bool;
+  mutable printing_coercions : bool;
+  mutable printing_raw_matching : bool;
+  mutable printing_no_notation : bool;
+  mutable printing_all : bool;
+  mutable printing_evar_instances : bool;
+  mutable printing_universes : bool;
+  mutable printing_full_all : bool
+}
+
+val printing_state : printing_state
+
+type reset_mark =
+  | ResetToId of Names.identifier
+  | ResetToState of Libnames.object_name
+
+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 -> Util.loc * Vernacexpr.vernac_expr
+val interp : bool -> string -> reset_info * (Util.loc * Vernacexpr.vernac_expr)
 val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
-val interp_and_replace : string -> (Util.loc * Vernacexpr.vernac_expr) * string
+val interp_and_replace : string -> 
+      (reset_info * (Util.loc * Vernacexpr.vernac_expr)) * string
 
-val is_tactic : Vernacexpr.vernac_expr -> bool
-val is_state_preserving : Vernacexpr.vernac_expr -> bool
+val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool
+val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool
+val is_vernac_goal_starting_command : Vernacexpr.vernac_expr -> bool
+val is_vernac_proof_ending_command : Vernacexpr.vernac_expr -> bool
 
 (* type hyp = (identifier * constr option * constr) * string *)
 
@@ -33,7 +70,7 @@ type goal = hyp list * concl
 
 val get_current_goals : unit -> goal list
 
-val get_current_pm_goal : unit -> hyp list * meta list
+val get_current_pm_goal : unit -> goal
 
 val get_current_goals_nb : unit -> int
 
@@ -41,13 +78,6 @@ val print_no_goal : unit -> string
 
 val process_exn : exn -> string*(Util.loc option)
 
-type reset_info = NoReset | Reset of Names.identifier * bool ref
-
-val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
-val reset_initial : unit -> unit
-val reset_to : identifier -> unit
-val reset_to_mod : identifier -> unit
-
 val hyp_menu : hyp -> (string * string) list
 val concl_menu : concl -> (string * string) list