diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-15 09:47:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-15 09:47:43 +0200 |
| commit | cbd28511526dfb561017c3d27a73598f6ce5f68d (patch) | |
| tree | a8786b32433caa850e24f67ab5a3aa85f29a683a /ide | |
| parent | 10e5883fed21f9631e1aa65adb7a7e62a529987f (diff) | |
| parent | 7402a7788b6a73bd5c0cb9078823d48e6f01a357 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.mli | 6 | ||||
| -rw-r--r-- | ide/coqide.ml | 4 | ||||
| -rw-r--r-- | ide/utf8_convert.mll | 2 | ||||
| -rw-r--r-- | ide/wg_ScriptView.ml | 2 |
4 files changed, 7 insertions, 7 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index a72c67b43..2dc5ad307 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 *) diff --git a/ide/coqide.ml b/ide/coqide.ml index e591f205f..5fdb4a2a4 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1059,8 +1059,8 @@ let build_ui () = ("Hide", "_Hide", `MISSING_IMAGE, ~callback:(fun _ -> let sess = notebook#current_term in toggle_proof_visibility sess.buffer sess.analyzed_view#get_insert), "Hide proof", "h"); *) - ("Previous", "_Previous", `GO_BACK, Nav.previous_occ, "Previous occurence", "less"); - ("Next", "_Next", `GO_FORWARD, Nav.next_occ, "Next occurence", "greater"); + ("Previous", "_Previous", `GO_BACK, Nav.previous_occ, "Previous occurrence", "less"); + ("Next", "_Next", `GO_FORWARD, Nav.next_occ, "Next occurrence", "greater"); ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f"); ] end; diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll index 621833dde..4ebf9a62e 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -12,7 +12,7 @@ } -(* Replace all occurences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *) +(* Replace all occurrences of \x{iiii} and \x{iiiiiiii} by UTF-8 valid chars *) let digit = ['0'-'9''A'-'Z''a'-'z'] let short = digit digit digit digit diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 14cbf92eb..b672e016b 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -141,7 +141,7 @@ object(self) (** We don't care about atomicity. Return: 1. `OK when there was no error, `FAIL otherwise - 2. `NOOP if no write occured, `WRITE otherwise + 2. `NOOP if no write occurred, `WRITE otherwise *) method private process_action = function | Insert ins -> |