diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-05-20 17:16:19 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-05-23 16:56:05 +0200 |
| commit | 16e1a879264b91cacf07635af39e2e710e1d6d53 (patch) | |
| tree | e87b460c77faddf007a1f0d9f9f408156d0ef687 /stm/stm.mli | |
| parent | cabf1f192065ae93cabf9bfe13f502a7597d0cfa (diff) | |
typos
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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 |