# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1358683174 18000
# Node ID b7419a10e52eac9b752d7b75e3bb18d52af64739
# Parent  07f2fb4d9b36174d3776124dd21212ed83503b60
Pass through Chapter 6

diff -r 07f2fb4d9b36 -r b7419a10e52e src/Subset.v
--- a/src/Subset.v	Sat Jan 19 10:45:04 2013 -0500
+++ b/src/Subset.v	Sun Jan 20 06:59:34 2013 -0500
@@ -161,9 +161,9 @@
 
 Locate "{ _ : _ | _ }".
 (** %\vspace{-.15in}% [[
-Notation
-"{ x : A  |  P }" := sig (fun x : A => P)
- ]]
+  Notation
+  "{ x : A  |  P }" := sig (fun x : A => P)
+   ]]
  *)
 
 Definition pred_strong2 (s : {n : nat | n > 0}) : nat :=
@@ -209,6 +209,12 @@
     | exist (S n') pf => exist _ n' (eq_refl _)
   end.
 
+(* begin hide *)
+(* begin thide *)
+Definition ugh := lt.
+(* end thide *)
+(* end hide *)
+
 Eval compute in pred_strong3 (exist _ 2 two_gt0).
 (** %\vspace{-.15in}% [[
      = exist (fun m : nat => 2 = S m) 1 (eq_refl 2)
@@ -370,7 +376,7 @@
     | S n' => n'
   end.
 
-(** Printing the resulting definition of [pred_strong6] yields a term very similar to what we built with [refine].  [Program] can save time in writing programs that use subset types.  Nonetheless, [refine] is often just as effective, and [refine] gives you more control over the form the final term takes, which can be useful when you want to prove additional theorems about your definition.  [Program] will sometimes insert type casts that can complicate theorem proving. *)
+(** Printing the resulting definition of [pred_strong6] yields a term very similar to what we built with [refine].  [Program] can save time in writing programs that use subset types.  Nonetheless, [refine] is often just as effective, and [refine] gives more control over the form the final term takes, which can be useful when you want to prove additional theorems about your definition.  [Program] will sometimes insert type casts that can complicate theorem proving. *)
 
 Eval compute in pred_strong6 two_gt0.
 (** %\vspace{-.15in}% [[
@@ -383,7 +389,7 @@
 
 (** * Decidable Proposition Types *)
 
-(** There is another type in the standard library which captures the idea of program values that indicate which of two propositions is true.%\index{Gallina terms!sumbool}% *)
+(** There is another type in the standard library that captures the idea of program values that indicate which of two propositions is true.%\index{Gallina terms!sumbool}% *)
 
 Print sumbool.
 (** %\vspace{-.15in}% [[