Mercurial > cpdt > repo

diff src/Equality.v @ 271:aa3c054afce0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Some bug fixes while working on JFR version
author Adam Chlipala <adamc@hcoop.net>
date Mon, 19 Apr 2010 16:49:26 -0400
parents c8508d277a00
children 19fbda8a8117
line wrap: on
line diff
--- a/src/Equality.v	Wed Feb 03 08:17:02 2010 -0500
+++ b/src/Equality.v	Mon Apr 19 16:49:26 2010 -0400
@@ -574,7 +574,7 @@
 
 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
 
-   Suppose that we want to use [UIP_refl'] to establish another lemma of the kind of we have run into several times so far. *)
+   Suppose that we want to use [UIP_refl'] to establish another lemma of the kind we have run into several times so far. *)
 
 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
   O = match pf with refl_equal => O end.