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

diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 4888ce4b1..e39eca0cb 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -9,7 +9,7 @@
 (** Normalisation functions for rational numbers. *)
 
 Require Export QArith_base.
-Require Import Zgcd_def Znumtheory.
+Require Import Znumtheory.
 
 (** First, a function that (tries to) build a positive back from a Z. *)
 
@@ -83,14 +83,13 @@ Proof.
   exists bb; auto with zarith.
   intros.
   inversion Hg1.
-  destruct (H6 (g*x)).
+  destruct (H6 (g*x)) as (x',Hx).
   rewrite Hg3.
   destruct H2 as (xa,Hxa); exists xa; rewrite Hxa; ring.
   rewrite Hg4.
   destruct H3 as (xb,Hxb); exists xb; rewrite Hxb; ring.
-  exists q.
-  apply Zmult_reg_l with g; auto.
-  pattern g at 1; rewrite H7; ring.
+  exists x'.
+  apply Zmult_reg_l with g; auto. rewrite Hx at 1; ring.
   (* /rel_prime *)
   unfold rel_prime in |- *.
   (* rel_prime *)
@@ -99,14 +98,13 @@ Proof.
   exists dd; auto with zarith.
   intros.
   inversion Hg'1.
-  destruct (H6 (g'*x)).
+  destruct (H6 (g'*x)) as (x',Hx).
   rewrite Hg'3.
   destruct H2 as (xc,Hxc); exists xc; rewrite Hxc; ring.
   rewrite Hg'4.
   destruct H3 as (xd,Hxd); exists xd; rewrite Hxd; ring.
-  exists q.
-  apply Zmult_reg_l with g'; auto.
-  pattern g' at 1; rewrite H7; ring.
+  exists x'.
+  apply Zmult_reg_l with g'; auto. rewrite Hx at 1; ring.
     (* /rel_prime *)
   assert (0<bb); [|auto with zarith].
   apply Zmult_gt_0_lt_0_reg_r with g.