From 16e1a879264b91cacf07635af39e2e710e1d6d53 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 May 2016 17:16:19 +0200 Subject: typos --- stm/stm.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'stm/stm.mli') diff --git a/stm/stm.mli b/stm/stm.mli index 4279921b3..6519a6254 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -125,7 +125,7 @@ val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ] (** read-eval-print loop compatible interface ****************************** **) (* Adds a new line to the document. It replaces the core of Vernac.interp. - [finish] is called as the last bit of this function is the system + [finish] is called as the last bit of this function if the system is running interactively (-emacs or coqtop). *) val interp : bool -> vernac_expr located -> unit @@ -135,7 +135,7 @@ val get_all_proof_names : unit -> Id.t list val get_current_proof_name : unit -> Id.t option val show_script : ?proof:Proof_global.closed_proof -> unit -> unit -(** Reverse dependency hooks *) +(* Hooks to be set by other Coq components in order to break file cycles *) val process_error_hook : Future.fix_exn Hook.t val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t -- cgit v1.2.3