Essai d'utilisation de 'where' pour les notations

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

1 files changed, 13 insertions, 11 deletions

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index b4ce93819..cd531f150 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -89,13 +89,14 @@ Hint Resolve n_Sn: core v62.
 Fixpoint plus (n m:nat) {struct n} : nat :=
   match n with
   | O => m
-  | S p => S (plus p m)
-  end.
+  | S p => S (p + m)
+  end
+
+where "n + m" := (plus n m) : nat_scope.
+
 Hint Resolve (f_equal2 plus): v62.
 Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
 
-Infix "+" := plus : nat_scope.
-
 Lemma plus_n_O : forall n:nat, n = n + 0.
 Proof.
   induction n; simpl in |- *; auto.
@@ -123,11 +124,12 @@ Qed.
 Fixpoint mult (n m:nat) {struct n} : nat :=
   match n with
   | O => 0
-  | S p => m + mult p m
-  end.
-Hint Resolve (f_equal2 mult): core v62.
+  | S p => m + p * m
+  end
 
-Infix "*" := mult : nat_scope.
+where "n * m" := (mult n m) : nat_scope.
+
+Hint Resolve (f_equal2 mult): core v62.
 
 Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Proof.
@@ -149,10 +151,10 @@ Fixpoint minus (n m:nat) {struct n} : nat :=
   match n, m with
   | O, _ => 0
   | S k, O => S k
-  | S k, S l => minus k l
-  end. 
+  | S k, S l => k - l
+  end
 
-Infix "-" := minus : nat_scope.
+where "n - m" := (minus n m) : nat_scope.
 
 (** Definition of the usual orders, the basic properties of [le] and [lt] 
     can be found in files Le and Lt *)