Mercurial > cpdt > repo
diff src/Equality.v @ 271:aa3c054afce0
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.