# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1272469203 14400
# Node ID 19fbda8a8117184f1c1929862e5970fc3f0f6d19
# Parent  aa3c054afce0a271dff30b3efbc086030997c6a3
Typo fix in Equality, found proof-reading tutorial

diff -r aa3c054afce0 -r 19fbda8a8117 src/Equality.v
--- a/src/Equality.v	Mon Apr 19 16:49:26 2010 -0400
+++ b/src/Equality.v	Wed Apr 28 11:40:03 2010 -0400
@@ -669,7 +669,7 @@
 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
 
 (* begin thide *)
-(** Assuming axioms (like axiom K and [JMeq_eq]) is a hazardous business.  The due diligence associated with it is necessarily global in scope, since two axioms may be consistent alone but inconsistent together.  It turns out that all of the major axioms proposed for reasoning about equality in Coq are logically equivalent, so that we only need to pick one to assert without proof.  In this section, we demonstrate this by showing how each the previous two sections' approaches reduces to the other logically.
+(** Assuming axioms (like axiom K and [JMeq_eq]) is a hazardous business.  The due diligence associated with it is necessarily global in scope, since two axioms may be consistent alone but inconsistent together.  It turns out that all of the major axioms proposed for reasoning about equality in Coq are logically equivalent, so that we only need to pick one to assert without proof.  In this section, we demonstrate this by showing how each of the previous two sections' approaches reduces to the other logically.
 
    To show that [JMeq] and its axiom let us prove [UIP_refl], we start from the lemma [UIP_refl'] from the previous section.  The rest of the proof is trivial. *)