# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223061104 14400
# Node ID 82a2189fa2834896c4e7dbd7dbda40281a3fe51a
# Parent  ec2c1830a7a13fa6d964c0d56999d32a4cbfacb8
Spell check

diff -r ec2c1830a7a1 -r 82a2189fa283 src/Subset.v
--- a/src/Subset.v	Fri Oct 03 15:10:30 2008 -0400
+++ b/src/Subset.v	Fri Oct 03 15:11:44 2008 -0400
@@ -233,7 +233,7 @@
     end); crush.
 Defined.
 
-(** We end the "proof" with [Defined] instead of [Qed], so that the definition we constructed remains visible.  This contrasts to the case of ending a proof with [Qed], where the details of the proof are hidden afterward.  Let us see what our prooof script constructed. *)
+(** We end the "proof" with [Defined] instead of [Qed], so that the definition we constructed remains visible.  This contrasts to the case of ending a proof with [Qed], where the details of the proof are hidden afterward.  Let us see what our proof script constructed. *)
 
 Print pred_strong4.
 (** [[