--- a/src/Equality.v	Wed Jul 25 17:50:12 2012 -0400
+++ b/src/Equality.v	Wed Jul 25 18:10:26 2012 -0400
@@ -200,7 +200,7 @@
       | _ :: ls' => fun mls idx =>
         match idx with
           | inl pf => match pf with
-                        | refl_equal => fst mls
+                        | eq_refl => fst mls
                       end
           | inr idx' => fhget ls' (snd mls) idx'
         end
@@ -244,13 +244,13 @@
   a0 : a = elm
   ============================
    match a0 in (_ = a2) return (C a2) with
-   | refl_equal => f a1
+   | eq_refl => f a1
    end = f match a0 in (_ = a2) return (B a2) with
-           | refl_equal => a1
+           | eq_refl => a1
            end
        ]]
 
-   This seems like a trivial enough obligation.  The equality proof [a0] must be [refl_equal], since that is the only constructor of [eq].  Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
+   This seems like a trivial enough obligation.  The equality proof [a0] must be [eq_refl], since that is the only constructor of [eq].  Therefore, both the [match]es reduce to the point where the conclusion follows by reflexivity.
     [[
     destruct a0.
 ]]
@@ -261,11 +261,11 @@
 
     This is one of Coq's standard error messages for informing us that its heuristics for attempting an instance of an undecidable problem about dependent typing have failed.  We might try to nudge things in the right direction by stating the lemma that we believe makes the conclusion trivial.
     [[
-    assert (a0 = refl_equal _).
+    assert (a0 = eq_refl _).
 ]]
 
 <<
-The term "refl_equal ?98" has type "?98 = ?98"
+The term "eq_refl ?98" has type "?98 = ?98"
  while it is expected to have type "a = elm"
 >>
 
@@ -291,7 +291,7 @@
 
   (** It will be helpful to examine the proof terms generated by this sort of strategy.  A simpler example illustrates what is going on. *)
 
-  Lemma lemma1 : forall x (pf : x = elm), O = match pf with refl_equal => O end.
+  Lemma lemma1 : forall x (pf : x = elm), O = match pf with eq_refl => O end.
 (* begin thide *)
     simple destruct pf; reflexivity.
   Qed.
@@ -304,12 +304,12 @@
 lemma1 = 
 fun (x : A) (pf : x = elm) =>
 match pf as e in (_ = y) return (0 = match e with
-                                     | refl_equal => 0
+                                     | eq_refl => 0
                                      end) with
-| refl_equal => refl_equal 0
+| eq_refl => eq_refl 0
 end
      : forall (x : A) (pf : x = elm), 0 = match pf with
-                                          | refl_equal => 0
+                                          | eq_refl => 0
                                           end
  
     ]]
@@ -320,15 +320,15 @@
   Definition lemma1' :=
     fun (x : A) (pf : x = elm) =>
       match pf return (0 = match pf with
-                             | refl_equal => 0
+                             | eq_refl => 0
                            end) with
-        | refl_equal => refl_equal 0
+        | eq_refl => eq_refl 0
       end.
 (* end thide *)
 
   (** Surprisingly, what seems at first like a _simpler_ lemma is harder to prove. *)
 
-  Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with refl_equal => O end.
+  Lemma lemma2 : forall (x : A) (pf : x = x), O = match pf with eq_refl => O end.
 (* begin thide *)
     (** %\vspace{-.25in}%[[
     simple destruct pf.
@@ -346,15 +346,15 @@
   Definition lemma2 :=
     fun (x : A) (pf : x = x) =>
       match pf return (0 = match pf with
-                             | refl_equal => 0
+                             | eq_refl => 0
                            end) with
-        | refl_equal => refl_equal 0
+        | eq_refl => eq_refl 0
       end.
 (* end thide *)
 
   (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
 
-  Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
+  Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
 (* begin thide *)
     (** %\vspace{-.25in}%[[
     simple destruct pf.
@@ -371,13 +371,13 @@
      [[
   Definition lemma3' :=
     fun (x : A) (pf : x = x) =>
-      match pf as pf' in (_ = x') return (pf' = refl_equal x') with
-        | refl_equal => refl_equal _
+      match pf as pf' in (_ = x') return (pf' = eq_refl x') with
+        | eq_refl => eq_refl _
       end.
 ]]
 
 <<
-The term "refl_equal x'" has type "x' = x'" while it is expected to have type
+The term "eq_refl x'" has type "x' = x'" while it is expected to have type
  "x = x'"
 >>
 
@@ -385,14 +385,14 @@
 
      Nonetheless, it turns out that, with one catch, we _can_ prove this lemma. *)
 
-  Lemma lemma3 : forall (x : A) (pf : x = x), pf = refl_equal x.
+  Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
     intros; apply UIP_refl.
   Qed.
 
   Check UIP_refl.
   (** %\vspace{-.15in}% [[
 UIP_refl
-     : forall (U : Type) (x : U) (p : x = x), p = refl_equal x
+     : 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_. *)
@@ -426,7 +426,7 @@
 Streicher_K = 
 fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
      : forall (U : Type) (x : U) (P : x = x -> Prop),
-       P (refl_equal x) -> forall p : x = x, P p
+       P (eq_refl x) -> forall p : x = x, P p
   ]]
 
   This is the unfortunately named %\index{axiom K}``%#"#Streicher's axiom K,#"#%''% which says that a predicate on properly typed equality proofs holds of all such proofs if it holds of reflexivity. *)
@@ -477,7 +477,7 @@
     (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3),
     fhapp hls1 (fhapp hls2 hls3)
     = match pf in (_ = ls) return fhlist _ ls with
-        | refl_equal => fhapp (fhapp hls1 hls2) hls3
+        | eq_refl => fhapp (fhapp hls1 hls2) hls3
       end.
     induction ls1; crush.
 
@@ -486,7 +486,7 @@
   ============================
    fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3 =
    match pf in (_ = ls) return (fhlist B ls) with
-   | refl_equal => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
+   | eq_refl => fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3
    end
        ]]
 
@@ -519,7 +519,7 @@
    fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
      (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
    match pf in (_ = ls) return (fhlist B ls) with
-   | refl_equal =>
+   | eq_refl =>
        (a0,
        fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
          (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
@@ -544,7 +544,7 @@
    fhapp (ls1:=ls1) (ls2:=ls2 ++ ls3) b
      (fhapp (ls1:=ls2) (ls2:=ls3) hls2 hls3)) =
    match pf in (_ = ls) return (fhlist B ls) with
-   | refl_equal =>
+   | eq_refl =>
        (a0,
        fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
          (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
@@ -558,12 +558,12 @@
   ============================
    (a0,
    match pf' in (_ = ls) return (fhlist B ls) with
-   | refl_equal =>
+   | eq_refl =>
        fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
          (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3
    end) =
    match pf in (_ = ls) return (fhlist B ls) with
-   | refl_equal =>
+   | eq_refl =>
        (a0,
        fhapp (ls1:=ls1 ++ ls2) (ls2:=ls3)
          (fhapp (ls1:=ls1) (ls2:=ls2) b hls2) hls3)
@@ -577,10 +577,10 @@
    forall f : fhlist B ((ls1 ++ ls2) ++ ls3),
    (a0,
    match pf' in (_ = ls) return (fhlist B ls) with
-   | refl_equal => f
+   | eq_refl => f
    end) =
    match pf in (_ = ls) return (fhlist B ls) with
-   | refl_equal => (a0, f)
+   | eq_refl => (a0, f)
    end
         ]]
 
@@ -595,10 +595,10 @@
      (f : fhlist B ((ls1 ++ ls2) ++ ls3)),
    (a0,
    match pf'0 in (_ = ls) return (fhlist B ls) with
-   | refl_equal => f
+   | eq_refl => f
    end) =
    match pf0 in (_ = ls) return (fhlist B ls) with
-   | refl_equal => (a0, f)
+   | eq_refl => (a0, f)
    end
         ]]
 
@@ -614,10 +614,10 @@
      (f : fhlist B (ls1 ++ ls2 ++ ls3)),
    (a0,
    match pf'0 in (_ = ls) return (fhlist B ls) with
-   | refl_equal => f
+   | eq_refl => f
    end) =
    match pf0 in (_ = ls) return (fhlist B ls) with
-   | refl_equal => (a0, f)
+   | eq_refl => (a0, f)
    end
         ]]
 
@@ -650,11 +650,11 @@
 
 Infix "==" := JMeq (at level 70, no associativity).
 
-(* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == refl_equal x *)
+(* EX: Prove UIP_refl' : forall (A : Type) (x : A) (pf : x = x), pf == eq_refl x *)
 (* begin thide *)
-Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
-  match pf return (pf == refl_equal _) with
-    | refl_equal => JMeq_refl _
+Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == eq_refl x :=
+  match pf return (pf == eq_refl _) with
+    | eq_refl => JMeq_refl _
   end.
 (* end thide *)
 
@@ -663,7 +663,7 @@
    Suppose that we want to use [UIP_refl'] to establish another lemma of the kind we have run into several times so far. *)
 
 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
-  O = match pf with refl_equal => O end.
+  O = match pf with eq_refl => O end.
 (* begin thide *)
   intros; rewrite (UIP_refl' pf); reflexivity.
 Qed.
@@ -862,14 +862,14 @@
 
    To show that [JMeq] and its axiom let us prove [UIP_refl], we start from the lemma [UIP_refl'] from the previous section.  The rest of the proof is trivial. *)
 
-Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
+Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = eq_refl x.
   intros; rewrite (UIP_refl' pf); reflexivity.
 Qed.
 
 (** The other direction is perhaps more interesting.  Assume that we only have the axiom of the [Eqdep] module available.  We can define [JMeq] in a way that satisfies the same interface as the combination of the [JMeq] module's inductive definition and axiom. *)
 
 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
-  exists pf : B = A, x = match pf with refl_equal => y end.
+  exists pf : B = A, x = match pf with eq_refl => y end.
 
 Infix "===" := JMeq' (at level 70, no associativity).
 
@@ -879,7 +879,7 @@
 
 (** remove printing exists *)
 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
-  intros; unfold JMeq'; exists (refl_equal A); reflexivity.
+  intros; unfold JMeq'; exists (eq_refl A); reflexivity.
 Qed.
 
 (** printing exists $\exists$ *)
@@ -892,7 +892,7 @@
   (** [[
   H : exists pf : A = A,
         x = match pf in (_ = T) return T with
-            | refl_equal => y
+            | eq_refl => y
             end
   ============================
    x = y
@@ -903,7 +903,7 @@
   (** [[
   x0 : A = A
   H : x = match x0 in (_ = T) return T with
-          | refl_equal => y
+          | eq_refl => y
           end
   ============================
    x = y
@@ -915,7 +915,7 @@
   x0 : A = A
   ============================
    match x0 in (_ = T) return T with
-   | refl_equal => y
+   | eq_refl => y
    end = y
       ]]
       *)