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

1 files changed, 4 insertions, 4 deletions

diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 33181e32a..57277b489 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -347,22 +347,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 *)