diff options
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 56 |
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 |