Miscellaneous typos, spacing, US spelling in comments or variable names.

6 files changed, 8 insertions, 8 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 09299f31d..4f32fdce8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -477,7 +477,7 @@ let rec execute env cstr =
       let j' = execute env1 c3 in
         judge_of_letin env name j1 j2 j'
 
-    | Cast (c,k, t) ->
+    | Cast (c,k,t) ->
       let cj = execute env c in
       let tj = execute_type env t in
         judge_of_cast env cj k tj
diff --git a/lib/future.mli b/lib/future.mli
index de2282ae9..adc15e49c 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -91,13 +91,13 @@ val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
  * When a future enters the environment a corresponding hook is run to perform
  * some work.  If this fails, then its failure has to be annotated with the
  * same state id that corresponds to the future computation end.  I.e. Qed
- * is split into two parts, the lazy one (the future) and the eagher one
+ * is split into two parts, the lazy one (the future) and the eager one
  * (the hook), both performing some computations for the same state id. *)
 val fix_exn_of : 'a computation -> fix_exn
 
 (* Run remotely, returns the function to assign.
    If not blocking (the default) it raises NotReady if forced before the
-   delage assigns it. *)
+   delegate assigns it. *)
 type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 val create_delegate :
   ?blocking:bool -> name:string ->
diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml
index 81f02b66d..b9165aa81 100644
--- a/proofs/logic_monad.ml
+++ b/proofs/logic_monad.ml
@@ -188,7 +188,7 @@ struct
       shape of the monadic type is reminiscent of that of the
       continuation monad transformer.
 
-      The paper also contains the rational for the [split] abstraction.
+      The paper also contains the rationale for the [split] abstraction.
 
       An explanation of how to derive such a monad from mathematical
       principles can be found in "Kan Extensions for Program
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 028116049..fcb706cc8 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -94,7 +94,7 @@ val start_dependent_proof :
 val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
- * Both access the current proof state. The formes is supposed to be
+ * Both access the current proof state. The former is supposed to be
  * chained with a computation that completed the proof *)
 
 type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
diff --git a/stm/stm.ml b/stm/stm.ml
index 5bb46fd36..88a1fbbf4 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -639,7 +639,7 @@ end = struct (* {{{ *)
     proof,
     Summary.project_summary (States.summary_of_state system) summary_pstate
 
-  let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
+  let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable)
 
   let is_cached ?(cache=`No) id =
     if Stateid.equal id !cur_id then
@@ -1912,7 +1912,7 @@ let init () =
   Backtrack.record ();
   Slaves.init ();
   if Flags.async_proofs_is_master () then begin
-    prerr_endline "Initialising workers";
+    prerr_endline "Initializing workers";
     Query.init ();
     let opts = match !Flags.async_proofs_private_flags with
       | None -> []
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 356ccdcc6..670447452 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -8,7 +8,7 @@
 
 (** The Coq main module. The following function [start] will parse the
    command line, print the banner, initialize the load path, load the input
-   state, load the files given on the command line, load the ressource file,
+   state, load the files given on the command line, load the resource file,
    produce the output state if any, and finally will launch [Coqloop.loop]. *)
 
 val init_toplevel : string list -> unit