From 927b92eb8e1abf7ff1978f812b602b276d69dd27 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 16 Oct 2012 23:05:56 +0000
Subject: Removing redundant definition of case_eq (see #2919). Thanks to F.
 Blanqui for spotting it out.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15897 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rfunctions.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 4724d0e531..5eb34324ed 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -525,9 +525,6 @@ Qed.
 (*******************************)
 (*i Due to L.Thery i*)
 
-Ltac case_eq name :=
-  generalize (eq_refl name); pattern name at -1; case name.
-
 Definition powerRZ (x:R) (n:Z) :=
   match n with
     | Z0 => 1
-- 
cgit v1.2.3