diff options
Diffstat (limited to 'ide/coq.mli')
-rw-r--r-- | ide/coq.mli | 42 |
1 files changed, 13 insertions, 29 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index a1bea931..af17c0e9 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coq.mli 11126 2008-06-13 18:45:04Z herbelin $ i*) +(*i $Id: coq.mli 13323 2010-07-24 15:57:30Z herbelin $ 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 |