--- a/src/DataStruct.v	Fri Jul 27 15:41:06 2012 -0400
+++ b/src/DataStruct.v	Fri Jul 27 16:47:28 2012 -0400
@@ -161,7 +161,9 @@
 (* end thide *)
 
 (* begin hide *)
+(* begin thide *)
 Definition map' := map.
+(* end thide *)
 (* end hide *)
 
 (** Our [get] function is also quite easy to reason about.  We show how with a short example about an analogue to the list [map] function. *)
@@ -237,7 +239,8 @@
         match mem in member ls' return (match ls' with
                                           | nil => Empty_set
                                           | x' :: ls'' =>
-                                            B x' -> (member ls'' -> B elm) -> B elm
+                                            B x' -> (member ls'' -> B elm)
+                                            -> B elm
                                         end) with
           | MFirst _ => fun x _ => x
           | MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
@@ -472,7 +475,9 @@
   (** By pattern-matching on the equality proof [pf], we make that equality known to the type-checker.  Exactly why this works can be seen by studying the definition of equality. *)
 
   (* begin hide *)
-  Definition foo := (@eq, @eq_refl).
+  (* begin thide *)
+  Definition foo := @eq_refl.
+  (* end thide *)
   (* end hide *)
 
   Print eq.