From dbfadc5cb31e2857d2fba3ea46f320485a718af3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 14 Apr 2003 00:37:06 +0000
Subject: Local 'o'

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

diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 42293730ce..068b9367b1 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -34,7 +34,7 @@ Notation "- x" := (opp_fct x) (at level 0) : Rfun_scope
 Infix "*" mult_fct (at level 3, left associativity) : Rfun_scope.
 Infix "-" minus_fct (at level 4, left associativity) : Rfun_scope.
 Infix "/" div_fct (at level 3, left associativity) : Rfun_scope.
-Notation "f1 'o' f2" := (comp f1 f2) (at level 2, right associativity)
+Notation Local "f1 'o' f2" := (comp f1 f2) (at level 2, right associativity)
   : Rfun_scope.
 Notation "/ x" := (inv_fct x) (at level 0): Rfun_scope
   V8only (at level 30, left associativity).
-- 
cgit v1.2.3