In abstract parts of theories/Numbers, plus/times becomes add/mul,

for increased consistency with bignums parts 

(commit part I: content of files)



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

1 files changed, 8 insertions, 8 deletions

diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 64f597af0a..0b35868884 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -24,9 +24,9 @@ Definition NZeq := (@eq nat).
 Definition NZ0 := 0.
 Definition NZsucc := S.
 Definition NZpred := pred.
-Definition NZplus := plus.
+Definition NZadd := plus.
 Definition NZminus := minus.
-Definition NZtimes := mult.
+Definition NZmul := mult.
 
 Theorem NZeq_equiv : equiv nat NZeq.
 Proof (eq_equiv nat).
@@ -51,7 +51,7 @@ Proof.
 congruence.
 Qed.
 
-Add Morphism NZplus with signature NZeq ==> NZeq ==> NZeq as NZplus_wd.
+Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
 Proof.
 congruence.
 Qed.
@@ -61,7 +61,7 @@ Proof.
 congruence.
 Qed.
 
-Add Morphism NZtimes with signature NZeq ==> NZeq ==> NZeq as NZtimes_wd.
+Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
 Proof.
 congruence.
 Qed.
@@ -78,12 +78,12 @@ Proof.
 reflexivity.
 Qed.
 
-Theorem NZplus_0_l : forall n : nat, 0 + n = n.
+Theorem NZadd_0_l : forall n : nat, 0 + n = n.
 Proof.
 reflexivity.
 Qed.
 
-Theorem NZplus_succ_l : forall n m : nat, (S n) + m = S (n + m).
+Theorem NZadd_succ_l : forall n m : nat, (S n) + m = S (n + m).
 Proof.
 reflexivity.
 Qed.
@@ -98,12 +98,12 @@ Proof.
 intros n m; induction n m using nat_double_ind; simpl; auto. apply NZminus_0_r.
 Qed.
 
-Theorem NZtimes_0_l : forall n : nat, 0 * n = 0.
+Theorem NZmul_0_l : forall n : nat, 0 * n = 0.
 Proof.
 reflexivity.
 Qed.
 
-Theorem NZtimes_succ_l : forall n m : nat, S n * m = n * m + m.
+Theorem NZmul_succ_l : forall n m : nat, S n * m = n * m + m.
 Proof.
 intros n m; now rewrite plus_comm.
 Qed.