# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1228138340 18000
# Node ID cadeb49dc1ef4eb2d60034d32084d82aa646a424
# Parent  a35eaec19781a97ebda5e21f0e5c96e4e34f7ff5
Fix typo

diff -r a35eaec19781 -r cadeb49dc1ef src/Equality.v
--- a/src/Equality.v	Fri Nov 28 14:21:38 2008 -0500
+++ b/src/Equality.v	Mon Dec 01 08:32:20 2008 -0500
@@ -25,7 +25,7 @@
 
 (** We have seen many examples so far where proof goals follow "by computation."  That is, we apply computational reduction rules to reduce the goal to a normal form, at which point it follows trivially.  Exactly when this works and when it does not depends on the details of Coq's %\textit{%#<i>#definitional equality#</i>#%}%.  This is an untyped binary relation appearing in the formal metatheory of CIC.  CIC contains a typing rule allowing the conclusion $E : T$ from the premise $E : T'$ and a proof that $T$ and $T'$ are definitionally equal.
 
-   The [cbv] tactic will help us illustrate the rules of Coq's definitional equality.  We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [1] when applied to [0]. *)
+   The [cbv] tactic will help us illustrate the rules of Coq's definitional equality.  We redefine the natural number predecessor function in a somewhat convoluted way and construct a manual proof that it returns [0] when applied to [1]. *)
 
 Definition pred' (x : nat) :=
   match x with