--- a/src/Subset.v	Wed Aug 01 15:52:50 2012 -0400
+++ b/src/Subset.v	Wed Aug 01 16:09:37 2012 -0400
@@ -85,7 +85,7 @@
      : nat
  ]]
 
-%\smallskip{}%One aspect in particular of the definition of [pred_strong1] may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.
+One aspect in particular of the definition of [pred_strong1] may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.
 
 %\vspace{-.15in}%[[
 Definition pred_strong1' (n : nat) (pf : n > 0) : nat :=
@@ -153,7 +153,7 @@
     exist : forall x : A, P x -> sig P
 ]]
 
-%\smallskip{}%The family [sig] is a Curry-Howard twin of [ex], except that [sig] is in [Type], while [ex] is in [Prop].  That means that [sig] values can survive extraction, while [ex] proofs will always be erased.  The actual details of extraction of [sig]s are more subtle, as we will see shortly.
+The family [sig] is a Curry-Howard twin of [ex], except that [sig] is in [Type], while [ex] is in [Prop].  That means that [sig] values can survive extraction, while [ex] proofs will always be erased.  The actual details of extraction of [sig]s are more subtle, as we will see shortly.
 
 We rewrite [pred_strong1], using some syntactic sugar for subset types. *)
 
@@ -301,7 +301,7 @@
      : forall n : nat, n > 0 -> {m : nat | n = S m}
 ]]
 
-%\smallskip{}%We see the code we entered, with some proofs filled in.  The first proof obligation, the second argument to [False_rec], is filled in with a nasty-looking proof term that we can be glad we did not enter by hand.  The second proof obligation is a simple reflexivity proof. *)
+We see the code we entered, with some proofs filled in.  The first proof obligation, the second argument to [False_rec], is filled in with a nasty-looking proof term that we can be glad we did not enter by hand.  The second proof obligation is a simple reflexivity proof. *)
 
 Eval compute in pred_strong4 two_gt0.
 (** %\vspace{-.15in}% [[
@@ -309,7 +309,7 @@
      : {m : nat | 2 = S m}
      ]]
 
-  %\smallskip{}%A tactic modifier called %\index{tactics!abstract}%[abstract] can be helpful for producing shorter terms, by automatically abstracting subgoals into named lemmas. *)
+  A tactic modifier called %\index{tactics!abstract}%[abstract] can be helpful for producing shorter terms, by automatically abstracting subgoals into named lemmas. *)
 
 (* begin thide *)
 Definition pred_strong4' : forall n : nat, n > 0 -> {m : nat | n = S m}.
@@ -358,7 +358,7 @@
      : {m : nat | 2 = S m}
      ]]
 
-  %\smallskip{}%One other alternative is worth demonstrating.  Recent Coq versions include a facility called %\index{Program}%[Program] that streamlines this style of definition.  Here is a complete implementation using [Program].%\index{Vernacular commands!Obligation Tactic}\index{Vernacular commands!Program Definition}% *)
+  One other alternative is worth demonstrating.  Recent Coq versions include a facility called %\index{Program}%[Program] that streamlines this style of definition.  Here is a complete implementation using [Program].%\index{Vernacular commands!Obligation Tactic}\index{Vernacular commands!Program Definition}% *)
 
 Obligation Tactic := crush.
 
@@ -376,7 +376,7 @@
      : {m : nat | 2 = S m}
      ]]
 
-%\smallskip{}%In this case, we see that the new definition yields the same computational behavior as before. *)
+In this case, we see that the new definition yields the same computational behavior as before. *)
 
 
 (** * Decidable Proposition Types *)
@@ -421,7 +421,7 @@
      : {2 = 3} + {2 <> 3}
      ]]
 
-%\smallskip{}%Note that the %\coqdocnotation{%#<tt>#Yes#</tt>#%}% and %\coqdocnotation{%#<tt>#No#</tt>#%}% notations are hiding proofs establishing the correctness of the outputs.
+Note that the %\coqdocnotation{%#<tt>#Yes#</tt>#%}% and %\coqdocnotation{%#<tt>#No#</tt>#%}% notations are hiding proofs establishing the correctness of the outputs.
 
    Our definition extracts to reasonable OCaml code. *)
 
@@ -529,7 +529,7 @@
      : {In 3 (1 :: 2 :: nil)} + {~ In 3 (1 :: 2 :: nil)}
      ]]
 
-%\smallskip{}%[In_dec] has a reasonable extraction to OCaml. *)
+[In_dec] has a reasonable extraction to OCaml. *)
 
 Extraction In_dec.
 (* end thide *)
@@ -596,7 +596,7 @@
      : {{m | 0 = S m}}
      ]]
 
-     %\smallskip{}%Because we used [maybe], one valid implementation of the type we gave [pred_strong7] would return [??] in every case.  We can strengthen the type to rule out such vacuous implementations, and the type family %\index{Gallina terms!sumor}%[sumor] from the standard library provides the easiest starting point.  For type [A] and proposition [B], [A + {B}] desugars to [sumor A B], whose values are either values of [A] or proofs of [B]. *)
+     Because we used [maybe], one valid implementation of the type we gave [pred_strong7] would return [??] in every case.  We can strengthen the type to rule out such vacuous implementations, and the type family %\index{Gallina terms!sumor}%[sumor] from the standard library provides the easiest starting point.  For type [A] and proposition [B], [A + {B}] desugars to [sumor A B], whose values are either values of [A] or proofs of [B]. *)
 
 Print sumor.
 (** %\vspace{-.15in}% [[
@@ -604,7 +604,7 @@
     inleft : A -> A + {B} | inright : B -> A + {B}
 ]]
 
-%\smallskip{}%We add notations for easy use of the [sumor] constructors.  The second notation is specialized to [sumor]s whose [A] parameters are instantiated with regular subset types, since this is how we will use [sumor] below. *)
+We add notations for easy use of the [sumor] constructors.  The second notation is specialized to [sumor]s whose [A] parameters are instantiated with regular subset types, since this is how we will use [sumor] below. *)
 
 Notation "!!" := (inright _ _).
 Notation "[|| x ||]" := (inleft _ [x]).
@@ -776,7 +776,7 @@
      : {{t | hasType (Plus (Nat 1) (Bool false)) t}}
      ]]
 
-%\smallskip{}%The type checker also extracts to some reasonable OCaml code. *)
+The type checker also extracts to some reasonable OCaml code. *)
 
 Extraction typeCheck.
 
@@ -929,4 +929,4 @@
        {(forall t : type, ~ hasType (Plus (Nat 1) (Bool false)) t)}
        ]]
 
-%\smallskip{}%The results of simplifying calls to [typeCheck'] look deceptively similar to the results for [typeCheck], but now the types of the results provide more information. *)
+The results of simplifying calls to [typeCheck'] look deceptively similar to the results for [typeCheck], but now the types of the results provide more information. *)