Mise en place d'ensembles de notations symboliques pour nat, Z et R

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3125 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 2 insertions, 23 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 7af85c65ad..13c17aabb5 100755
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -18,19 +18,3 @@ Require Export Between.
 Require Export Minus.
 Require Export Peano_dec.
 Require Export Compare_dec.
-
-Axiom My_special_variable : nat -> nat.
-
-Grammar nat number :=.
-
-Grammar constr constr10 :=
-  natural_nat [ nat:number($c) ] -> [$c].
-
-Grammar constr pattern :=
-  natural_pat [ nat:pat_number($c) ] -> [$c].
-
-Syntax constr
-  level 10:
-  S [ (S $p) ] -> [$p:"nat_printer":9]
-| O [ O ] -> [ "0" ]
-.
diff --git a/theories/Arith/ArithSyntax.v b/theories/Arith/ArithSyntax.v
deleted file mode 100644
index cd762d4253..0000000000
--- a/theories/Arith/ArithSyntax.v
+++ /dev/null
@@ -1,6 +0,0 @@
-Infix 4 "+" plus.
-Infix 3 "*" mult.
-Infix 1 "<=" le.
-Infix 1 "<" lt.
-Infix 1 ">=" ge.
-(* Infix 1 ">" gt.*)
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 5263cb3757..3ad37d13a4 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -12,7 +12,8 @@
 
 Require Le.
 Require Lt.
-Require ArithSyntax.
+
+Import nat_scope.
 
 Lemma plus_sym : (n,m:nat)(n+m)=(m+n).
 Proof.