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

for increased consistency with bignums parts 

(commit part II: names of files + additional translation minus --> sub)



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

6 files changed, 23 insertions, 23 deletions

diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZAdd.v
index 6fb72ed4a9..9c852bf908 100644
--- a/theories/Numbers/NatInt/NZPlus.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -13,7 +13,7 @@
 Require Import NZAxioms.
 Require Import NZBase.
 
-Module NZPlusPropFunct (Import NZAxiomsMod : NZAxiomsSig).
+Module NZAddPropFunct (Import NZAxiomsMod : NZAxiomsSig).
 Module Export NZBasePropMod := NZBasePropFunct NZAxiomsMod.
 Open Local Scope NatIntScope.
 
@@ -82,10 +82,10 @@ intros n m p. rewrite (NZadd_comm n p); rewrite (NZadd_comm m p).
 apply NZadd_cancel_l.
 Qed.
 
-Theorem NZminus_1_r : forall n : NZ, n - 1 == P n.
+Theorem NZsub_1_r : forall n : NZ, n - 1 == P n.
 Proof.
-intro n; rewrite NZminus_succ_r; now rewrite NZminus_0_r.
+intro n; rewrite NZsub_succ_r; now rewrite NZsub_0_r.
 Qed.
 
-End NZPlusPropFunct.
+End NZAddPropFunct.
 
diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 00d178c0d9..d1caa83eeb 100644
--- a/theories/Numbers/NatInt/NZPlusOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -13,7 +13,7 @@
 Require Import NZAxioms.
 Require Import NZOrder.
 
-Module NZPlusOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
+Module NZAddOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
 Module Export NZOrderPropMod := NZOrderPropFunct NZOrdAxiomsMod.
 Open Local Scope NatIntScope.
 
@@ -162,5 +162,5 @@ Proof.
 intros n m H; apply NZadd_le_cases; now rewrite NZadd_0_l.
 Qed.
 
-End NZPlusOrderPropFunct.
+End NZAddOrderPropFunct.
 
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 516cf5b42b..1ef7809866 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -20,11 +20,11 @@ Parameter Inline NZ0 : NZ.
 Parameter Inline NZsucc : NZ -> NZ.
 Parameter Inline NZpred : NZ -> NZ.
 Parameter Inline NZadd : NZ -> NZ -> NZ.
-Parameter Inline NZminus : NZ -> NZ -> NZ.
+Parameter Inline NZsub : NZ -> NZ -> NZ.
 Parameter Inline NZmul : NZ -> NZ -> NZ.
 
-(* Unary minus (opp) is not defined on natural numbers, so we have it for
-integers only *)
+(* Unary subtraction (opp) is not defined on natural numbers, so we have 
+   it for integers only *)
 
 Axiom NZeq_equiv : equiv NZ NZeq.
 Add Relation NZ NZeq
@@ -36,7 +36,7 @@ as NZeq_rel.
 Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
 Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
 Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
-Add Morphism NZminus with signature NZeq ==> NZeq ==> NZeq as NZminus_wd.
+Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
 Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
 
 Delimit Scope NatIntScope with NatInt.
@@ -48,7 +48,7 @@ Notation S := NZsucc.
 Notation P := NZpred.
 Notation "1" := (S 0) : NatIntScope.
 Notation "x + y" := (NZadd x y) : NatIntScope.
-Notation "x - y" := (NZminus x y) : NatIntScope.
+Notation "x - y" := (NZsub x y) : NatIntScope.
 Notation "x * y" := (NZmul x y) : NatIntScope.
 
 Axiom NZpred_succ : forall n : NZ, P (S n) == n.
@@ -60,8 +60,8 @@ Axiom NZinduction :
 Axiom NZadd_0_l : forall n : NZ, 0 + n == n.
 Axiom NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m).
 
-Axiom NZminus_0_r : forall n : NZ, n - 0 == n.
-Axiom NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m).
+Axiom NZsub_0_r : forall n : NZ, n - 0 == n.
+Axiom NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m).
 
 Axiom NZmul_0_l : forall n : NZ, 0 * n == 0.
 Axiom NZmul_succ_l : forall n m : NZ, S n * m == n * m + m.
diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZMul.v
index 9f93e0a1bf..7d9b1aabd3 100644
--- a/theories/Numbers/NatInt/NZTimes.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -11,10 +11,10 @@
 (*i $Id$ i*)
 
 Require Import NZAxioms.
-Require Import NZPlus.
+Require Import NZAdd.
 
-Module NZTimesPropFunct (Import NZAxiomsMod : NZAxiomsSig).
-Module Export NZPlusPropMod := NZPlusPropFunct NZAxiomsMod.
+Module NZMulPropFunct (Import NZAxiomsMod : NZAxiomsSig).
+Module Export NZAddPropMod := NZAddPropFunct NZAxiomsMod.
 Open Local Scope NatIntScope.
 
 Theorem NZmul_0_r : forall n : NZ, n * 0 == 0.
@@ -76,5 +76,5 @@ Proof.
 intro n; rewrite NZmul_comm; apply NZmul_1_l.
 Qed.
 
-End NZTimesPropFunct.
+End NZMulPropFunct.
 
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index ebb2a9b5d0..ae5e2d4447 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -11,10 +11,10 @@
 (*i $Id$ i*)
 
 Require Import NZAxioms.
-Require Import NZPlusOrder.
+Require Import NZAddOrder.
 
-Module NZTimesOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
-Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZOrdAxiomsMod.
+Module NZMulOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
+Module Export NZAddOrderPropMod := NZAddOrderPropFunct NZOrdAxiomsMod.
 Open Local Scope NatIntScope.
 
 Theorem NZmul_lt_pred :
@@ -307,4 +307,4 @@ now apply -> NZle_succ_l.
 apply NZadd_pos_pos; now apply NZlt_succ_diag_r.
 Qed.
 
-End NZTimesOrderPropFunct.
+End NZMulOrderPropFunct.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index f76fa94808..d8eaeb99c2 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -11,11 +11,11 @@
 (*i $Id$ i*)
 
 Require Import NZAxioms.
-Require Import NZTimes.
+Require Import NZMul.
 Require Import Decidable.
 
 Module NZOrderPropFunct (Import NZOrdAxiomsMod : NZOrdAxiomsSig).
-Module Export NZTimesPropMod := NZTimesPropFunct NZAxiomsMod.
+Module Export NZMulPropMod := NZMulPropFunct NZAxiomsMod.
 Open Local Scope NatIntScope.
 
 Ltac le_elim H := rewrite NZlt_eq_cases in H; destruct H as [H | H].