# HG changeset patch # User Adam Chlipala # Date 1442663082 14400 # Node ID 429e95d23b26dde3e3b8fe79c2a53a488603e045 # Parent 582bf8d4ce51b6f91bd4e37ba22be93ddcaeedfe Typo fix diff -r 582bf8d4ce51 -r 429e95d23b26 src/InductiveTypes.v --- a/src/InductiveTypes.v Sat Aug 15 15:59:02 2015 -0400 +++ b/src/InductiveTypes.v Sat Sep 19 07:44:42 2015 -0400 @@ -944,7 +944,7 @@ There is no command like [Scheme] that will implement an improved principle for us. In general, it takes creativity to figure out _good_ ways to incorporate nested uses of different type families. Now that we know how to implement induction principles manually, we are in a position to apply just such creativity to this problem. -Many induction principles for types with nested used of [list] could benefit from a unified predicate capturing the idea that some property holds of every element in a list. By defining this generic predicate once, we facilitate reuse of library theorems about it. (Here, we are actually duplicating the standard library's [Forall] predicate, with a different implementation, for didactic purposes.) *) +Many induction principles for types with nested uses of [list] could benefit from a unified predicate capturing the idea that some property holds of every element in a list. By defining this generic predicate once, we facilitate reuse of library theorems about it. (Here, we are actually duplicating the standard library's [Forall] predicate, with a different implementation, for didactic purposes.) *) Section All. Variable T : Set.