Fixing typos - Part 2

13 files changed, 15 insertions, 15 deletions

diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 542a05fd25..a1c49bee95 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -105,7 +105,7 @@ value init_coq_vm(value unit) /* ML */
     init_coq_interpreter();
     
     /* Some predefined pointer code.
-     * It is typically contained in accumlator blocks whose tag is 0 and thus
+     * It is typically contained in accumulator blocks whose tag is 0 and thus
      * scanned by the GC, so make it look like an OCaml block. */
     value accu_block = (value) coq_stat_alloc(2 * sizeof(value));
     Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black);        \
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 95f88c0306..fc7d1a54f2 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -226,7 +226,7 @@ let unfold_red kn =
  * this constant or abstraction.
  *  * i_tab is the cache table of the results
  *
- * ref_value_cache searchs in the tab, otherwise uses i_repr to
+ * ref_value_cache searches in the tab, otherwise uses i_repr to
  * compute the result and store it in the table. If the constant can't
  * be unfolded, returns None, but does not store this failure.  * This
  * doesn't take the RESET into account. You mustn't keep such a table
@@ -645,7 +645,7 @@ and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with
 and comp_subs el s =
   Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s
 
-(* This function defines the correspondance between constr and
+(* This function defines the correspondence between constr and
    fconstr. When we find a closure whose substitution is the identity,
    then we directly return the constr to avoid possibly huge
    reallocation. *)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 1a790eaed6..60185464c5 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -200,7 +200,7 @@ val whd_val : clos_infos -> clos_tab -> fconstr -> constr
 val whd_stack :
   clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack
 
-(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding
+(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
     to the conversion of the eta expansion of t, considered as an inhabitant
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 69f004307d..90fbcb8ae3 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -386,7 +386,7 @@ let rec is_tailcall = function
   | Klabel _ :: c -> is_tailcall c
   | _ -> None
 
-(* Extention of the continuation *)
+(* Extension of the continuation *)
 
 (* Add a Kpop n instruction in front of a continuation *)
 let rec add_pop n = function
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 7fc57cdb8a..aa5878c9d7 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -141,7 +141,7 @@ val mkRef : GlobRef.t Univ.puniverses -> constr
     [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] 
     presented as describe in [ci].
 
-    [p] stucture is [fun args x -> "return clause"]
+    [p] structure is [fun args x -> "return clause"]
 
     [ac]{^ ith} element is ith constructor case presented as 
     {e lambda construct_args (without params). case_term } *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 36ee952099..860d19fe26 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -22,11 +22,11 @@ type engagement = set_predicativity
 (** {6 Representation of constants (Definition/Axiom) } *)
 
 (** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives
-    and constants hiding inductives are implicitely polymorphic when
+    and constants hiding inductives are implicitly polymorphic when
     applied to parameters, on the universes appearing in the whnf of
     their parameters and their conclusion, in a template style.
     
-    In truely universe polymorphic mode, we always use RegularArity.
+    In truly universe polymorphic mode, we always use RegularArity.
 *)
 
 type template_arity = {
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d9335d39b5..ca7086a3e4 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -166,7 +166,7 @@ let make_subst env =
         (* template, it is identity substitution  otherwise (ie. when u is *)
         (* already in the domain of the substitution) [remember_subst] will *)
         (* update its image [x] by [sup x u] in order not to forget the *)
-        (* dependency in [u] that remains to be fullfilled. *)
+        (* dependency in [u] that remains to be fulfilled. *)
         make (remember_subst u subst) (sign, exp, [])
     | _sign, [], _ ->
         (* Uniform parameters are exhausted *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 2de5faa6df..72393d0081 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -188,7 +188,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
       in
       let new_equiv = add_delta_resolver equiv new_mb.mod_delta in
       (* we propagate the new equality in the rest of the signature
-	 with the identity substitution accompagned by the new resolver*)
+         with the identity substitution accompanied by the new resolver*)
       let id_subst = map_mp mp' mp' new_mb.mod_delta in
       let new_after = subst_structure id_subst after in
       before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4fdd7ab334..472fddb829 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -515,7 +515,7 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
      "Module M:=P." or "Module M. Include P. End M."
     We need to perform two operations to compute the body of M.
     - The first one is applying the substitution {P <- M} on the type of P
-    - The second one is strenghtening. *)
+    - The second one is strengthening. *)
 
 let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
   |NoFunctor struc ->
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index f25f24512d..93632da110 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -13,7 +13,7 @@ val of_uint : int -> t
 
 val hash : t -> int
 
-     (* convertion to a string *)
+     (* conversion to a string *)
 val to_string : t -> string
 val of_string : string -> t
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index b1bbc25fe6..2b88d6884d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -726,7 +726,7 @@ let univ_level_rem u v min =
   | Some u' -> if Level.equal u u' then min else v
   | None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v
 
-(* Is u mentionned in v (or equals to v) ? *)
+(* Is u mentioned in v (or equals to v) ? *)
 
 
 (**********************************************************************)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index db178c4bb0..ddb204dd52 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -163,7 +163,7 @@ val super : Universe.t -> Universe.t
 
 val universe_level : Universe.t -> Level.t option
 
-(** [univ_level_mem l u] Is l is mentionned in u ? *)
+(** [univ_level_mem l u] Is l is mentioned in u ? *)
 
 val univ_level_mem : Level.t -> Universe.t -> bool
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 777a207013..5e3a3c3347 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -12,7 +12,7 @@ open Univ
 open Constr
 
 (*******************************************)
-(* Initalization of the abstract machine ***)
+(* Initialization of the abstract machine ***)
 (* Necessary for [relaccu_tbl]             *)
 (*******************************************)