aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-10-14 10:39:55 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-10-14 10:39:55 +0200
commitf617aeef08441e83b13f839ce767b840fddbcf7d (patch)
tree9a0c914031262f5491745d9773d7c2a0e5bdaa41 /theories/Lists
parented95f122f3c68becc09c653471dc2982b346d343 (diff)
Fix some typos.
Diffstat (limited to 'theories/Lists')
-rw-r--r--theories/Lists/List.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 0ace6938b..fe18686e2 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.