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, 2 insertions, 2 deletions

diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index e90977e3d7..eb46e69de0 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -25,12 +25,12 @@ only one time. *)
 Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod.
 
 (* Here we probably need to re-prove all axioms declared in NAxioms.v to
-make sure that the definitions like N, S and plus are unfolded in them,
+make sure that the definitions like N, S and add are unfolded in them,
 since unfolding is done only inside a functor. In fact, we'll do it in the
 files that prove the corresponding properties. In those files, we will also
 rename properties proved in NZ files by removing NZ from their names. In
 this way, one only has to consult, for example, NPlus.v to see all
-available properties for plus, i.e., one does not have to go to NAxioms.v
+available properties for add, i.e., one does not have to go to NAxioms.v
 for axioms and NZPlus.v for theorems. *)
 
 Theorem succ_wd : forall n1 n2 : N, n1 == n2 -> S n1 == S n2.