From ebb3fe944b6bd1cd363e3348465d7ea2fd85c62c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 3 Jun 2008 00:04:16 +0000
Subject: 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
---
 theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'theories/Numbers/Integer/SpecViaZ')

diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index bb56e6997c..e1f04e45ad 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -42,7 +42,7 @@ Definition NZ0 := Z.zero.
 Definition NZsucc := Z.succ.
 Definition NZpred := Z.pred.
 Definition NZadd := Z.add.
-Definition NZminus := Z.sub.
+Definition NZsub := Z.sub.
 Definition NZmul := Z.mul.
 
 Theorem NZeq_equiv : equiv Z.t Z.eq.
@@ -71,7 +71,7 @@ Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
 
-Add Morphism NZminus with signature Z.eq ==> Z.eq ==> Z.eq as NZminus_wd.
+Add Morphism NZsub with signature Z.eq ==> Z.eq ==> Z.eq as NZsub_wd.
 Proof.
 intros; zsimpl; f_equal; assumption.
 Qed.
@@ -154,12 +154,12 @@ Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZminus_0_r : forall n, n - 0 == n.
+Theorem NZsub_0_r : forall n, n - 0 == n.
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
 
-Theorem NZminus_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).
+Theorem NZsub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m).
 Proof.
 intros; zsimpl; auto with zarith.
 Qed.
-- 
cgit v1.2.3