--- a/src/Coinductive.v	Thu Jul 26 19:05:12 2012 -0400
+++ b/src/Coinductive.v	Fri Jul 27 15:41:06 2012 -0400
@@ -543,10 +543,9 @@
 
 Definition var := nat.
 
-(** We define a type [vars] of maps from variables to values.  To define a function [set] for setting a variable's value in a map, we import the [Arith] module from Coq's standard library, and we use its function [beq_nat] for comparing natural numbers. *)
+(** We define a type [vars] of maps from variables to values.  To define a function [set] for setting a variable's value in a map, we use the standard library function [beq_nat] for comparing natural numbers. *)
 
 Definition vars := var -> nat.
-Require Import Arith.
 Definition set (vs : vars) (v : var) (n : nat) : vars :=
   fun v' => if beq_nat v v' then n else vs v'.
 

--- a/src/Equality.v	Thu Jul 26 19:05:12 2012 -0400
+++ b/src/Equality.v	Fri Jul 27 15:41:06 2012 -0400
@@ -413,18 +413,16 @@
      : forall (U : Type) (x : U) (p : x = x), p = eq_refl x
      ]]
 
-     The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library.  Do the Coq authors know of some clever trick for building such proofs that we have not seen yet?  If they do, they did not use it for this proof.  Rather, the proof is based on an _axiom_, the term [Eq_rect_eq.eq_rect_eq] below. *)
+     The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library.  Do the Coq authors know of some clever trick for building such proofs that we have not seen yet?  If they do, they did not use it for this proof.  Rather, the proof is based on an _axiom_, the term [eq_rect_eq] below. *)
 
-  (* begin hide *)
-  Definition ere := eq_rect_eq.
-  (* end hide *)
-
+(* begin hide *)
+  Import Eq_rect_eq.
+(* end hide *)
   Print eq_rect_eq.
   (** %\vspace{-.15in}% [[
-eq_rect_eq = 
-fun U : Type => Eq_rect_eq.eq_rect_eq U
-     : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
-       x = eq_rect p Q x p h
+*** [ eq_rect_eq : 
+forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
+x = eq_rect p Q x p h ]
       ]]
 
       The axiom %\index{Gallina terms!eq\_rect\_eq}%[eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered.  The term [eq_rect] is the automatically generated recursion principle for [eq].  Calling [eq_rect] is another way of [match]ing on an equality proof.  The proof we match on is the argument [h], and [x] is the body of the [match].  The statement of [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed.  We can see this intuition better in code by asking Coq to simplify the theorem statement with the [compute] reduction strategy (which, by the way, applies all applicable rules of the definitional equality presented in this chapter's first section). *)
@@ -463,6 +461,10 @@
 
 End fhlist_map.
 
+(* begin hide *)
+Require Eqdep_dec.
+(* end hide *)
+
 (** It is worth remarking that it is possible to avoid axioms altogether for equalities on types with decidable equality.  The [Eqdep_dec] module of the standard library contains a parametric proof of [UIP_refl] for such cases.  To simplify presentation, we will stick with the axiom version in the rest of this chapter. *)
 
 

--- a/src/Subset.v	Thu Jul 26 19:05:12 2012 -0400
+++ b/src/Subset.v	Fri Jul 27 15:41:06 2012 -0400
@@ -402,7 +402,7 @@
 Notation "'No'" := (right _ _).
 Notation "'Reduce' x" := (if x then Yes else No) (at level 50).
 
-(** The [Reduce] notation is notable because it demonstrates how [if] is overloaded in Coq.  The [if] form actually works when the test expression has any two-constructor inductive type.  Moreover, in the [then] and [else] branches, the appropriate constructor arguments are bound.  This is important when working with [sumbool]s, when we want to have the proof stored in the test expression available when proving the proof obligations generated in the appropriate branch.
+(** The %\coqdocnotation{%#<tt>#Reduce#</tt>#%}% notation is notable because it demonstrates how [if] is overloaded in Coq.  The [if] form actually works when the test expression has any two-constructor inductive type.  Moreover, in the [then] and [else] branches, the appropriate constructor arguments are bound.  This is important when working with [sumbool]s, when we want to have the proof stored in the test expression available when proving the proof obligations generated in the appropriate branch.
 
 Now we can write [eq_nat_dec], which compares two natural numbers, returning either a proof of their equality or a proof of their inequality. *)
 
@@ -429,7 +429,7 @@
      ]]
      *)
 
-(** Note that the [Yes] and [No] 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. *)
 

--- a/src/Universes.v	Thu Jul 26 19:05:12 2012 -0400
+++ b/src/Universes.v	Fri Jul 27 15:41:06 2012 -0400
@@ -776,6 +776,10 @@
     end.
 Qed.
 
+(* begin hide *)
+Require Eqdep_dec.
+(* end hide *)
+
 (** These corollaries are special cases of proof irrelevance.  In developments that only need proof irrelevance for equality, there is no need to assert full irrelevance.
 
    Another facet of proof irrelevance is that, like excluded middle, it is often provable for specific propositions.  For instance, [UIP] is provable whenever the type [A] has a decidable equality operation.  The module [Eqdep_dec] of the standard library contains a proof.  A similar phenomenon applies to other notable cases, including less-than proofs.  Thus, it is often possible to use proof irrelevance without asserting axioms.
@@ -844,6 +848,10 @@
 
   This axiom lets us convert a relational specification [R] into a function implementing that specification.  We need only prove that [R] is truly a function.  An alternate, stronger formulation applies to cases where [R] maps each input to one or more outputs.  We also simplify the statement of the theorem by considering only non-dependent function types. *)
 
+(* begin hide *)
+Require RelationalChoice.
+(* end hide *)
+
 Require Import ClassicalChoice.
 Check choice.
 (** %\vspace{-.15in}% [[