From 12a55370b525185858aed77af4ef1dc0d5cf4e7e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 4 Dec 2013 13:57:57 +0100
Subject: Improved the presentation of the proof of UIP_refl_nat.

---
 theories/Logic/Eqdep_dec.v | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 9bde2d6415..8979421da1 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -358,17 +358,12 @@ Proof.
             end x).
     destruct x; reflexivity.
   - specialize IHn with (f_equal pred x).
-    change eq_refl with
-           (match (@eq_refl _ n) in _ = n' return S n = S n' with
-            | eq_refl => eq_refl
-            end).
+    change eq_refl with (f_equal S (@eq_refl _ n)).
     rewrite <- IHn; clear IHn.
     change (match S n as n' return S n = n' -> Prop with
             | 0 => fun _ => True
             | S n' => fun x =>
-                x = match f_equal pred x in _ = n' return S n = S n' with
-                    | eq_refl => eq_refl
-                    end
+                x = f_equal S (f_equal pred x)
             end x).
   pattern (S n) at 2 3, x.
   destruct x; reflexivity.
-- 
cgit v1.2.3