From 7f97b79b6372a115070f399d8804b57baa76ca74 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 31 Mar 2003 22:17:09 +0000
Subject: Ajout Implicit Variable Type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3827 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/RIneq.v      | 2 ++
 theories/Reals/Rbasic_fun.v | 2 ++
 theories/Reals/Rseries.v    | 2 ++
 3 files changed, 6 insertions(+)

(limited to 'theories/Reals')

diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 09de5a8e89..a09ec91742 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -20,6 +20,8 @@ Import nat_scope.
 Import Z_scope.
 Import R_scope.
 
+Implicit Variable Type r:R.
+
 (***************************************************************************)
 (**       Instantiating Ring tactic on reals                               *)
 (***************************************************************************)
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 5de4bd1fdc..57de5d5b92 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -18,6 +18,8 @@ Require R_Ifp.
 Require Fourier.
 Import R_scope.
 
+Implicit Variable Type r:R.
+
 (*******************************)
 (**          Rmin              *)
 (*******************************)
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 4496582225..f7f8cdddb6 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -13,6 +13,8 @@ Require Rfunctions.
 Require Classical.
 Require Compare.
 
+Implicit Variable Type r:R.
+
 (* classical is needed for [Un_cv_crit] *)
 (*********************************************************)
 (*           Definition of sequence and properties       *)
-- 
cgit v1.2.3