From 79fa2898ba31a2bfa484f3e9ac693ff714365758 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 10 Apr 2006 09:23:37 +0000
Subject: New unification can solve the problem without eta-expansion, but is
 bugguy with it. Temporary fix.

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

diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v
index 77fefdd7b6..e8bfe5ea55 100644
--- a/theories/Reals/Rtrigo_fun.v
+++ b/theories/Reals/Rtrigo_fun.v
@@ -61,10 +61,10 @@ intro; elim (IZN (up (/ eps - 1)) H0); intros; split with x; intros;
  rewrite (Rabs_Rabsolu (/ INR (S n))); cut (/ INR (S n) > 0).
 intro; rewrite (Rabs_pos_eq (/ INR (S n))).
 cut (/ eps - 1 < INR x).
-intro;
+intro ;
  generalize
   (Rlt_le_trans (/ eps - 1) (INR x) (INR n) H4
-     (le_INR x n ((fun (n m:nat) (H:(m >= n)%nat) => H) x n H2))); 
+     (le_INR x n H2)); 
  clear H4; intro; unfold Rminus in H4;
  generalize (Rplus_lt_compat_l 1 (/ eps + -1) (INR n) H4);
  replace (1 + (/ eps + -1)) with (/ eps); [ clear H4; intro | ring ].
-- 
cgit v1.2.3