diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
| commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
| tree | 074182834cb406d1304aec4233718564a9c06ba1 /ide/coq.mli | |
| parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) | |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index a72c67b4..2dc5ad30 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -16,7 +16,7 @@ type coqtop Liveness management of coqtop is automatic. Whenever a coqtop dies abruptly, this module is responsible for relaunching the whole process. The reset handler set through [set_reset_handler] will be called after such an - abrupt failure. It is also called when explicitely requesting coqtop to + abrupt failure. It is also called when explicitly requesting coqtop to reset. *) type 'a task @@ -29,7 +29,7 @@ type 'a task ([is_computing] will answer [true]), and any other task submission will be rejected by [try_grab]. - Any exception occuring within the task will trigger a coqtop reset. + Any exception occurring within the task will trigger a coqtop reset. Beware, because of the GTK scheduler, you never know when a task will actually be executed. If you need to sequentialize imperative actions, you @@ -43,7 +43,7 @@ val bind : 'a task -> ('a -> 'b task) -> 'b task (** Monadic binding of tasks *) val lift : (unit -> 'a) -> 'a task -(** Return the impertative computation waiting to be processed. *) +(** Return the imperative computation waiting to be processed. *) val seq : unit task -> 'a task -> 'a task (** Sequential composition *) |