From ad0c122b1665fedde52f51ecdebb9d04a12831a6 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 24 Jun 2011 15:50:17 +0000
Subject: Clean-up of Znumtheory, deletion of Zgcd_def

 In particular, we merge the old Zdivide (used to be an ad-hoc
 inductive predicate) and the new Z.divide (based on exists).
 Notations allow to do that (almost) transparently, the only
 impact is that the name picked by the system will not be "q"
 anymore when destructing a Z.divide. Some fragile scripts
 may have to be fixed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14239 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'theories/Numbers/Integer')

diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 44dd2c5934..6facd3c3a6 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -421,22 +421,22 @@ Qed.
 
 Lemma gcd_divide_l : forall n m, (gcd n m | n).
 Proof.
- intros n m. apply spec_divide. zify. apply Zgcd_divide_l.
+ intros n m. apply spec_divide. zify. apply Z.gcd_divide_l.
 Qed.
 
 Lemma gcd_divide_r : forall n m, (gcd n m | m).
 Proof.
- intros n m. apply spec_divide. zify. apply Zgcd_divide_r.
+ intros n m. apply spec_divide. zify. apply Z.gcd_divide_r.
 Qed.
 
 Lemma gcd_greatest : forall n m p, (p|n) -> (p|m) -> (p|gcd n m).
 Proof.
- intros n m p. rewrite !spec_divide. zify. apply Zgcd_greatest.
+ intros n m p. rewrite !spec_divide. zify. apply Z.gcd_greatest.
 Qed.
 
 Lemma gcd_nonneg : forall n m, 0 <= gcd n m.
 Proof.
- intros. zify. apply Zgcd_nonneg.
+ intros. zify. apply Z.gcd_nonneg.
 Qed.
 
 (** Bitwise operations *)
-- 
cgit v1.2.3