diff options
| author | barras | 2003-10-16 18:32:23 +0000 |
|---|---|---|
| committer | barras | 2003-10-16 18:32:23 +0000 |
| commit | ded597434229e373243f8d320ce51aaa4e35981f (patch) | |
| tree | f3ff61a8ac2fa445a642eaf574d2b562126dcd1f /theories/Reals | |
| parent | a69a28443fad9374d6ac9f3fe02d0270577fdba6 (diff) | |
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
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/RIneq.v | 2 |
1 files changed, 1 insertions, 1 deletions
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``. |