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

1 files changed, 12 insertions, 2 deletions

diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 5751f843c..248c8ce73 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.