From ded597434229e373243f8d320ce51aaa4e35981f Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 16 Oct 2003 18:32:23 +0000
Subject: lettac -> set suppression de la notation carre de R

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

(limited to 'theories/Reals')

diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 250ab423b7..cddc1a5416 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -410,7 +410,7 @@ Qed.
 
 (***********)
 Definition Rsqr:R->R:=[r:R]``r*r``.
-Notation "x ²" := (Rsqr x) (at level 2,left associativity).
+V7only[Notation "x ²" := (Rsqr x) (at level 2,left associativity).].
 
 (***********)
 Lemma Rsqr_O:(Rsqr ``0``)==``0``.
-- 
cgit v1.2.3