aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Lists')
-rw-r--r--theories/Lists/List.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 2437184a9..45306caf0 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