--- a/src/MoreDep.v	Wed Aug 01 16:09:37 2012 -0400
+++ b/src/MoreDep.v	Wed Aug 01 16:32:04 2012 -0400
@@ -87,18 +87,14 @@
 (* EX: Implement statically checked "car"/"hd" *)
 
 (** Now let us attempt a function that is surprisingly tricky to write.  In ML, the list head function raises an exception when passed an empty list.  With length-indexed lists, we can rule out such invalid calls statically, and here is a first attempt at doing so.  We write [???] as a placeholder for a term that we do not know how to write, not for any real Coq notation like those introduced two chapters ago.
-
 [[
 Definition hd n (ls : ilist (S n)) : A :=
   match ls with
     | Nil => ???
     | Cons _ h _ => h
   end.
- 
 ]]
-
 It is not clear what to write for the [Nil] case, so we are stuck before we even turn our function over to the type checker.  We could try omitting the [Nil] case:
-
 [[
 Definition hd n (ls : ilist (S n)) : A :=
   match ls with
@@ -141,7 +137,6 @@
                                   | 0 => unit
                                   | S _ => A
                                   end
- 
   ]]
   *)
 
@@ -243,7 +238,6 @@
 (** Despite the fancy type, the function definition is routine.  In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype.  The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case.  Remember that [eq_nat_dec] has a rich dependent type, rather than a simple boolean type.  Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple boolean from the [sumbool] that [eq_nat_dec] returns.
 
    We can implement our old favorite, a constant folding function, and prove it correct.  It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so.  Unsurprisingly, a first attempt leads to a type error.
-
 [[
 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) :=
   match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with
@@ -374,7 +368,6 @@
      ]]
 
      We would like to do a case analysis on [cfold e1], and we attempt that in the way that has worked so far.
-
      [[
   destruct (cfold e1).
 ]]
@@ -537,14 +530,14 @@
 (** Insertion relies on two balancing operations.  It will be useful to give types to these operations using a relative of the subset types from last chapter.  While subset types let us pair a value with a proof about that value, here we want to pair a value with another non-proof dependently typed value.  The %\index{Gallina terms!sigT}%[sigT] type fills this role. *)
 
 Locate "{ _ : _ & _ }".
-(** [[
+(** %\vspace{-.15in}%[[
 Notation            Scope     
 "{ x : A  & P }" := sigT (fun x : A => P)
 ]]
 *)
 
 Print sigT.
-(** [[
+(** %\vspace{-.15in}%[[
 Inductive sigT (A : Type) (P : A -> Type) : Type :=
     existT : forall x : A, P x -> sigT P
 ]]