Mercurial > cpdt > repo

diff src/DataStruct.v @ 296:559ec7328410

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Spelling errors found preparing JFR paper
author Adam Chlipala <adam@chlipala.net>
date Thu, 09 Dec 2010 14:39:49 -0500
parents 1b6c81e51799
children 7b38729be069
line wrap: on
line diff
--- a/src/DataStruct.v	Thu Dec 09 14:30:24 2010 -0500
+++ b/src/DataStruct.v	Thu Dec 09 14:39:49 2010 -0500
@@ -783,7 +783,7 @@
   end.
 
 (* begin thide *)
-(** To prove our final correctness theorem, it is useful to know that [cfoldCond] preserves expression meanings.  This lemma formalizes that property.  The proof is a standard mostly-automated one, with the only wrinkle being a guided instantation of the quantifiers in the induction hypothesis. *)
+(** To prove our final correctness theorem, it is useful to know that [cfoldCond] preserves expression meanings.  This lemma formalizes that property.  The proof is a standard mostly-automated one, with the only wrinkle being a guided instantiation of the quantifiers in the induction hypothesis. *)
 
 Lemma cfoldCond_correct : forall t (default : exp' t)
   n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t),