Merge branch 'v8.5'

3 files changed, 6 insertions, 6 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 2437184a93..45306caf08 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -69,7 +69,7 @@ Section Facts.
   Variable A : Type.
 
 
-  (** *** Genereric facts *)
+  (** *** Generic facts *)
 
   (** Discrimination *)
   Theorem nil_cons : forall (x:A) (l:list A), [] <> x :: l.
@@ -622,9 +622,9 @@ Section Elts.
   Qed.
 
 
-  (****************************************)
-  (** ** Counting occurences of a element *)
-  (****************************************)
+  (******************************************)
+  (** ** Counting occurrences of an element *)
+  (******************************************)
 
   Fixpoint count_occ (l : list A) (x : A) : nat :=
     match l with
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 4e28b5b905..f5e936cf01 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -19,7 +19,7 @@ Require Export DoubleType.
   arithmetic. In fact it is more general than that. The only reason
   for this use of 31 is the underlying mecanism for hardware-efficient
   computations by A. Spiwack. Apart from this, a switch to, say,
-  63-bit integers is now just a matter of replacing every occurences
+  63-bit integers is now just a matter of replacing every occurrences
   of 31 by 63. This is actually made possible by the use of
   dependently-typed n-ary constructions for the inductive type
   [int31], its constructor [I31] and any pattern matching on it.
diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v
index 6fdf0a2a5b..376620ddcd 100644
--- a/theories/Numbers/NaryFunctions.v
+++ b/theories/Numbers/NaryFunctions.v
@@ -15,7 +15,7 @@ Require Import List.
 (** * Generic dependently-typed operators about [n]-ary functions *)
 
 (** The type of [n]-ary function: [nfun A n B] is
-    [A -> ... -> A -> B] with [n] occurences of [A] in this type. *)
+    [A -> ... -> A -> B] with [n] occurrences of [A] in this type. *)
 
 Fixpoint nfun A n B :=
  match n with