# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1222622006 14400
# Node ID 31622083ad5d946275c1d3b156cc33f40d33fb2b
# Parent  422865e240b1e1cd8bf4bfd3145eb4f3c01dbd89
Spell-check

diff -r 422865e240b1 -r 31622083ad5d src/Predicates.v
--- a/src/Predicates.v	Sun Sep 28 12:44:50 2008 -0400
+++ b/src/Predicates.v	Sun Sep 28 13:13:26 2008 -0400
@@ -670,7 +670,7 @@
 Lemma even_contra' : forall n', even n' -> forall n, n' = S (n + n) -> False.
   induction 1; crush.
 
-  (** At this point, it is useful to consider all cases of [n] and [n0] being zero or nonzero.  Only one of these cases has any trickyness to it. *)
+  (** At this point, it is useful to consider all cases of [n] and [n0] being zero or nonzero.  Only one of these cases has any trickiness to it. *)
   destruct n; destruct n0; crush.
 
   (** [[