# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1345232395 14400
# Node ID 822442bf6d7fd00ffbb8ed2633a4274ba2e76c47
# Parent  f28bdd8414e0f29fad81f1be3c99ef0455911f78
Proofreading pass through Chapter 5

diff -r f28bdd8414e0 -r 822442bf6d7f src/Subset.v
--- a/src/Subset.v	Fri Aug 17 15:16:08 2012 -0400
+++ b/src/Subset.v	Fri Aug 17 15:39:55 2012 -0400
@@ -137,7 +137,7 @@
   | S n' -> n'
 </pre># *)
 
-(** The proof argument has disappeared!  We get exactly the OCaml code we would have written manually.  This is our first demonstration of the main technically interesting feature of Coq program extraction: program components of type [Prop] are erased systematically.
+(** The proof argument has disappeared!  We get exactly the OCaml code we would have written manually.  This is our first demonstration of the main technically interesting feature of Coq program extraction: proofs are erased systematically.
 
 We can reimplement our dependently typed [pred] based on%\index{subset types}% _subset types_, defined in the standard library with the type family %\index{Gallina terms!sig}%[sig]. *)