8 files changed, 12 insertions, 12 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 0a5bba39b9..7c2ecca89e 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -860,7 +860,7 @@ let compare_constructor_instances evd u u' =
     [u] up to existential variable instantiation and equalisable
     universes. The term [t] is interpreted in [sigma1] while [u] is
     interpreted in [sigma2]. The universe constraints in [sigma2] are
-    assumed to be an extention of those in [sigma1]. *)
+    assumed to be an extension of those in [sigma1]. *)
 let eq_constr_univs_test sigma1 sigma2 t u =
   (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
   let open Evd in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 8eaff8bd13..907be8eba2 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -208,7 +208,7 @@ val kind_of_term_upto : evar_map -> Constr.constr ->
     [u] up to existential variable instantiation and equalisable
     universes. The term [t] is interpreted in [sigma1] while [u] is
     interpreted in [sigma2]. The universe constraints in [sigma2] are
-    assumed to be an extention of those in [sigma1]. *)
+    assumed to be an extension of those in [sigma1]. *)
 val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
 
 (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index e0c24f049f..a504ee28e2 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -151,7 +151,7 @@ struct
   (** Double-continuation backtracking monads are reasonable folklore
       for "search" implementations (including the Tac interactive
       prover's tactics). Yet it's quite hard to wrap your head around
-      these.  I recommand reading a few times the "Backtracking,
+      these.  I recommend reading a few times the "Backtracking,
       Interleaving, and Terminating Monad Transformers" paper by
       O. Kiselyov, C. Shan, D. Friedman, and A. Sabry.  The peculiar
       shape of the monadic type is reminiscent of that of the
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 5c5a02d3fa..c00c90e5e9 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -31,7 +31,7 @@ type entry = (EConstr.constr * EConstr.types) list
     ide-s. *)
 (* spiwack: the type of [proofview] will change as we push more
    refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
+   new nearly identical function every time. Hence the generic name. *)
 (* In this version: returns the list of focused goals together with
    the [evar_map] context. *)
 let proofview p =
@@ -114,7 +114,7 @@ type focus_context = goal_with_state list * goal_with_state list
     instance, ide-s. *)
 (* spiwack: the type of [focus_context] will change as we push more
    refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
+   new nearly identical function every time. Hence the generic name. *)
 (* In this version: the goals in the context, as a "zipper" (the first
    list is in reversed order). *)
 let focus_context (left,right) =
@@ -123,7 +123,7 @@ let focus_context (left,right) =
 (** This (internal) function extracts a sublist between two indices,
     and returns this sublist together with its context: if it returns
     [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the
-    original list.  The focused list has lenght [j-i-1] and contains
+    original list.  The focused list has length [j-i-1] and contains
     the goals from number [i] to number [j] (both included) the first
     goal of the list being numbered [1].  [focus_sublist i j l] raises
     [IndexOutOfRange] if [i > length l], or [j > length l] or [j <
@@ -245,7 +245,7 @@ let tclUNIT = Proof.return
 (** Bind operation of the tactic monad. *)
 let tclBIND = Proof.(>>=)
 
-(** Interpretes the ";" (semicolon) of Ltac. As a monadic operation,
+(** Interprets the ";" (semicolon) of Ltac. As a monadic operation,
     it's a specialized "bind". *)
 let tclTHEN = Proof.(>>)
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index b7ff3ac432..60697c1611 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -24,7 +24,7 @@ type proofview
     ide-s. *)
 (* spiwack: the type of [proofview] will change as we push more
    refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
+   new nearly identical function every time. Hence the generic name. *)
 (* In this version: returns the list of focused goals together with
    the [evar_map] context. *)
 val proofview : proofview -> Evar.t list * Evd.evar_map
@@ -95,7 +95,7 @@ type focus_context
     instance, ide-s. *)
 (* spiwack: the type of [focus_context] will change as we push more
    refined functions to ide-s. This would be better than spawning a
-   new nearly identical function everytime. Hence the generic name. *)
+   new nearly identical function every time. Hence the generic name. *)
 (* In this version: the goals in the context, as a "zipper" (the first
    list is in reversed order). *)
 val focus_context : focus_context -> Evar.t list * Evar.t list
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 80eb9d0124..8ed75a8d00 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -252,7 +252,7 @@ module Giveup : Writer with type t = goal list = struct
   let put gs = Logical.put (true, gs)
 end
 
-(** Lens and utilies pertaining to the info trace *)
+(** Lens and utilities pertaining to the info trace *)
 module InfoL = struct
   let recording = Logical.(map (fun {P.trace} -> trace) current)
   let if_recording t =
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 3437b6ce77..f0c9fdb589 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -145,7 +145,7 @@ module Shelf : State with type t = goal list
     of the tactic. *)
 module Giveup : Writer with type t = goal list
 
-(** Lens and utilies pertaining to the info trace *)
+(** Lens and utilities pertaining to the info trace *)
 module InfoL : sig
   (** [record_trace t] behaves like [t] and compute its [info] trace. *)
   val record_trace : 'a Logical.t -> 'a Logical.t
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index fcbf305f9d..4f9f9ce6a5 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -353,7 +353,7 @@ let normalize_context_set g ctx us algs weak =
       noneqs Constraint.empty
   in
   (* Compute the left and right set of flexible variables, constraints
-     mentionning other variables remain in noneqs. *)
+     mentioning other variables remain in noneqs. *)
   let noneqs, ucstrsl, ucstrsr =
     Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) ->
       let lus = LMap.mem l us and rus = LMap.mem r us in