From 2c18a485ee162c63046b9d087bf74e6b3c4f7a06 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 11 Jul 2006 22:06:48 +0000
Subject: Ajout de quelques Arguments Scope pour simuler la récursivité du
 scope Rfun_scope en compensation (et anticipation) d'une suppression de la
 récursivité des délimiteurs de scope (ici %F)

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

diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 5751f843c9..248c8ce736 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -27,6 +27,18 @@ Definition div_real_fct (a:R) f (x:R) : R := a / f x.
 Definition comp f1 f2 (x:R) : R := f1 (f2 x).
 Definition inv_fct f (x:R) : R := / f x.
 
+Delimit Scope Rfun_scope with F.
+
+Arguments Scope plus_fct [Rfun_scope Rfun_scope R_scope].
+Arguments Scope mult_fct [Rfun_scope Rfun_scope R_scope].
+Arguments Scope minus_fct [Rfun_scope Rfun_scope R_scope].
+Arguments Scope div_fct [Rfun_scope Rfun_scope R_scope].
+Arguments Scope inv_fct [Rfun_scope R_scope].
+Arguments Scope opp_fct [Rfun_scope R_scope].
+Arguments Scope mult_real_fct [R_scope Rfun_scope R_scope].
+Arguments Scope div_real_fct [R_scope Rfun_scope R_scope].
+Arguments Scope comp [Rfun_scope Rfun_scope R_scope].
+
 Infix "+" := plus_fct : Rfun_scope.
 Notation "- x" := (opp_fct x) : Rfun_scope.
 Infix "*" := mult_fct : Rfun_scope.
@@ -36,8 +48,6 @@ Notation Local "f1 'o' f2" := (comp f1 f2)
   (at level 20, right associativity) : Rfun_scope.
 Notation "/ x" := (inv_fct x) : Rfun_scope.
 
-Delimit Scope Rfun_scope with F.
-
 Definition fct_cte (a x:R) : R := a.
 Definition id (x:R) := x.
 
-- 
cgit v1.2.3