Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2

13 files changed, 1174 insertions, 796 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 425528ee..786ade0e 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -9,7 +9,7 @@
 
 (* Finite map library.  *)
 
-(* $Id: FMapAVL.v 8899 2006-06-06 11:09:43Z jforest $ *)
+(* $Id: FMapAVL.v 8985 2006-06-23 16:12:45Z jforest $ *)
 
 (** This module implements map using AVL trees.
     It follows the implementation from Ocaml's standard library. *)
@@ -512,7 +512,7 @@ Proof.
  (* LT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt H1); intuition_in.
+ rewrite (IHt H0); intuition_in.
  (* EQ *)  
  inv avl.
  firstorder_in.
@@ -520,7 +520,7 @@ Proof.
  (* GT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt H2); intuition_in.
+ rewrite (IHt H1); intuition_in.
 Qed.
 
 Lemma add_bst : forall elt (m:t elt) x e, bst m -> avl m -> bst (add x e m).
@@ -530,13 +530,13 @@ Proof.
  (* lt_tree -> lt_tree (add ...) *)
  red; red in H4.
  intros.
- rewrite (add_in x y0 e H) in H1.
+ rewrite (add_in x y0 e H) in H0.
  intuition.
  eauto.
  (* gt_tree -> gt_tree (add ...) *)
- red; red in H5.
+ red; red in H4.
  intros.
- rewrite (add_in x y0 e H6) in H1.
+ rewrite (add_in x y0 e H5) in H0.
  intuition.
  apply lt_eq with x; auto.
 Qed.
@@ -591,9 +591,9 @@ Proof.
  inversion_clear H.
  destruct (IHp lh); auto.
  split; simpl in *. 
- rewrite_all H0. simpl in *.
+ rewrite_all e1. simpl in *.
  apply bal_avl; subst;auto; omega_max.
- rewrite_all H0;simpl in *;omega_bal.
+ rewrite_all e1;simpl in *;omega_bal.
 Qed.
 
 Lemma remove_min_avl : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> 
@@ -610,13 +610,13 @@ Proof.
  intuition_in.
  (* l = Node *)
  inversion_clear H.
- generalize (remove_min_avl H1).
+ generalize (remove_min_avl H0).
  
- rewrite_all H0; simpl; intros.
+ rewrite_all e1; simpl; intros.
  rewrite bal_in; auto.
- generalize (IHp lh y H1).
+ generalize (IHp lh y H0).
  intuition.
- inversion_clear H8; intuition.
+ inversion_clear H7; intuition.
 Qed.
 
 Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h) -> 
@@ -628,14 +628,14 @@ Proof.
  intuition_in; subst; auto.
  (* l = Node *)
  inversion_clear H.
- generalize (remove_min_avl H1).
- rewrite_all H0; simpl; intros.
+ generalize (remove_min_avl H0).
+ rewrite_all e1; simpl; intros.
  rewrite bal_mapsto; auto; unfold create.
  simpl in *;destruct (IHp lh y e').
  auto.
  intuition.
- inversion_clear H3; intuition.
- inversion_clear H10; intuition.
+ inversion_clear H2; intuition.
+ inversion_clear H9; intuition.
 Qed.
 
 Lemma remove_min_bst : forall elt (l:t elt) x e r h, 
@@ -643,14 +643,14 @@ Lemma remove_min_bst : forall elt (l:t elt) x e r h,
 Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
- inversion_clear H; inversion_clear H1.
+ inversion_clear H; inversion_clear H0.
  apply bal_bst; auto.
- rewrite_all H0;simpl in *;firstorder.
+ rewrite_all e1;simpl in *;firstorder.
  intro; intros.
  generalize (remove_min_in y H).
- rewrite_all H0; simpl in *.
+ rewrite_all e1; simpl in *.
  destruct 1.
- apply H4; intuition.
+ apply H3; intuition.
 Qed.
 
 Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, 
@@ -659,15 +659,15 @@ Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h,
 Proof.
  intros elt l x e r; functional induction (remove_min l x e r); simpl in *; intros.
  inv bst; auto.
- inversion_clear H; inversion_clear H1.
+ inversion_clear H; inversion_clear H0.
  intro; intro.
- rewrite_all H0;simpl in *.
- generalize (IHp lh H2 H); clear H7 H8 IHp.
+ rewrite_all e1;simpl in *.
+ generalize (IHp lh H1 H); clear H7 H6 IHp.
  generalize (remove_min_avl H).
  generalize (remove_min_in (fst m) H).
- rewrite H0; simpl; intros.
- rewrite (bal_in x e y H8 H6) in H1.
- destruct H7.
+ rewrite e1; simpl; intros.
+ rewrite (bal_in x e y H7 H5) in H0.
+ destruct H6.
  firstorder.
  apply lt_eq with x; auto.
  apply X.lt_trans with x; auto.
@@ -696,11 +696,11 @@ Lemma merge_avl_1 : forall elt (s1 s2:t elt), avl s1 -> avl s2 ->
 Proof.
  intros elt s1 s2; functional induction (merge s1 s2); simpl in *; intros.
  split; auto; avl_nns; omega_max.
- destruct s1;try contradiction;clear H1.
+ destruct s1;try contradiction;clear y.
  split; auto; avl_nns; simpl in *; omega_max.
- destruct s1;try contradiction;clear H1.
+ destruct s1;try contradiction;clear y.
  generalize (remove_min_avl_1 H0).
- rewrite H2; simpl;destruct 1.
+ rewrite e3; simpl;destruct 1.
  split.
  apply bal_avl; auto.
  simpl; omega_max.
@@ -719,13 +719,13 @@ Proof.
  intros elt s1 s2; functional induction (merge s1 s2);intros.
  intuition_in.
  intuition_in.
- destruct s1;try contradiction;clear H1.
+ destruct s1;try contradiction;clear y.
 (*  rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. *)
- replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto].
+ replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite e3; auto].
  rewrite bal_in; auto.
- generalize (remove_min_avl H4); rewrite H2; simpl; auto.
- generalize (remove_min_in y H4); rewrite H2; simpl; intro.
- rewrite H1; intuition.
+ generalize (remove_min_avl H2); rewrite e3; simpl; auto.
+ generalize (remove_min_in y0 H2); rewrite e3; simpl; intro.
+ rewrite H3; intuition.
 Qed.
 
 Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
@@ -734,13 +734,13 @@ Proof.
  intros elt s1 s2; functional induction (@merge elt s1 s2); intros.
  intuition_in.
  intuition_in.
- destruct s1;try contradiction;clear H1.
- replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H2; auto].
+ destruct s1;try contradiction;clear y.
+ replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite e3; auto].
  rewrite bal_mapsto; auto; unfold create.
- generalize (remove_min_avl H4); rewrite H2; simpl; auto.
- generalize (remove_min_mapsto y e0 H4); rewrite H2; simpl; intro.
- rewrite H1; intuition (try subst; auto).
- inversion_clear H1; intuition.
+ generalize (remove_min_avl H2); rewrite e3; simpl; auto.
+ generalize (remove_min_mapsto y0 e H2); rewrite e3; simpl; intro.
+ rewrite H3; intuition (try subst; auto).
+ inversion_clear H3; intuition.
 Qed.
 
 Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
@@ -751,13 +751,13 @@ Proof.
 
  apply bal_bst; auto.
  destruct s1;try contradiction.
- generalize (remove_min_bst H3); rewrite H2; simpl in *; auto.
+ generalize (remove_min_bst H1); rewrite e3; simpl in *; auto.
  destruct s1;try contradiction.
  intro; intro.
- apply H5; auto.
- generalize (remove_min_in x H4); rewrite H2; simpl; intuition.
+ apply H3; auto.
+ generalize (remove_min_in x H2); rewrite e3; simpl; intuition.
  destruct s1;try contradiction.
- generalize (remove_min_gt_tree H3); rewrite H2; simpl; auto.
+ generalize (remove_min_gt_tree H1); rewrite e3; simpl; auto.
 Qed. 
 
 (** * Deletion *)
@@ -779,18 +779,18 @@ Proof.
  split; auto; omega_max.
  (* LT *)
  inv avl.
- destruct (IHt H1).
+ destruct (IHt H0).
  split. 
  apply bal_avl; auto.
  omega_max.
  omega_bal.
  (* EQ *)
  inv avl. 
- generalize (merge_avl_1 H1 H2 H3).
+ generalize (merge_avl_1 H0 H1 H2).
  intuition omega_max.
  (* GT *)
  inv avl.
- destruct (IHt H2).
+ destruct (IHt H1).
  split. 
  apply bal_avl; auto.
  omega_max.
@@ -809,17 +809,17 @@ Proof.
  intros elt s x; functional induction (@remove elt x s); simpl; intros.
  intuition_in.
  (* LT *)
- inv avl; inv bst; clear H0.
+ inv avl; inv bst; clear e1.
  rewrite bal_in; auto.
- generalize (IHt y0 H1); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H0); intuition; [ order | order | intuition_in ].
  (* EQ *)
- inv avl; inv bst; clear H0.
+ inv avl; inv bst; clear e1.
  rewrite merge_in; intuition; [ order | order | intuition_in ].
  elim H9; eauto.
  (* GT *)
- inv avl; inv bst; clear H0.
+ inv avl; inv bst; clear e1.
  rewrite bal_in; auto.
- generalize (IHt y0 H6); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H5); intuition; [ order | order | intuition_in ].
 Qed.
 
 Lemma remove_bst : forall elt (s:t elt) x, bst s -> avl s -> bst (remove x s).
@@ -830,7 +830,7 @@ Proof.
  inv avl; inv bst.
  apply bal_bst; auto.
  intro; intro.
- rewrite (remove_in x y0 H1) in H; auto.
+ rewrite (remove_in x y0 H0) in H; auto.
  destruct H; eauto.
  (* EQ *)
  inv avl; inv bst.
@@ -839,7 +839,7 @@ Proof.
  inv avl; inv bst.
  apply bal_bst; auto.
  intro; intro.
- rewrite (remove_in x y0 H6) in H; auto.
+ rewrite (remove_in x y0 H5) in H; auto.
  destruct H; eauto.
 Qed.
 
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index c671ba82..067f5a3e 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FMapList.v 8899 2006-06-06 11:09:43Z jforest $ *)
+(* $Id: FMapList.v 9035 2006-07-09 15:42:09Z herbelin $ *)
 
 (** * Finite map library *)
 
@@ -20,8 +20,6 @@ Require Import FMapInterface.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Arguments Scope list [type_scope].
-
 Module Raw (X:OrderedType).
 
 Module E := X.
@@ -161,14 +159,14 @@ Proof.
  inversion 2.
 
  inversion_clear 2.
- clear H0;compute in H1; destruct H1;order.
- clear H0;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H1)); compute; order.
+ clear e1;compute in H0; destruct H0;order.
+ clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order.
 
- clear H0;inversion_clear 2.
+ clear e1;inversion_clear 2.
  compute in H0; destruct H0; intuition congruence. 
  generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute; order.
  
- clear H0; do 2 inversion_clear 1; auto.
+ clear e1; do 2 inversion_clear 1; auto.
  compute in H2; destruct H2; order.
 Qed.
 
@@ -197,7 +195,7 @@ Lemma add_2 : forall m x y e e',
 Proof.
  intros m x  y e e'. 
  generalize y e; clear y e; unfold PX.MapsTo.
- functional induction (add x e' m) ;simpl;auto;  clear H0.
+ functional induction (add x e' m) ;simpl;auto;  clear e0.
  subst;auto.
 
  intros y' e'' eqky';  inversion_clear 1;  destruct H0; simpl in *.
@@ -214,9 +212,9 @@ Proof.
  intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo.
  functional induction (add x e' m);simpl; intros.
  apply (In_inv_3 H0); compute; auto.
- apply (In_inv_3 H1); compute; auto.
- constructor 2; apply (In_inv_3 H1); compute; auto. 
- inversion_clear H1; auto.
+ apply (In_inv_3 H0); compute; auto.
+ constructor 2; apply (In_inv_3 H0); compute; auto. 
+ inversion_clear H0; auto.
 Qed.
 
 
@@ -265,13 +263,13 @@ Proof.
  red; inversion 1; inversion H1.
 
  apply Sort_Inf_NotIn with x0; auto.
- clear H0;constructor; compute; order.
+ clear e0;constructor; compute; order.
  
- clear H0;inversion_clear Hm.
+ clear e0;inversion_clear Hm.
  apply Sort_Inf_NotIn with x0; auto. 
  apply Inf_eq with (k',x0);auto; compute; apply X.eq_trans with x; auto.
 
- clear H0;inversion_clear Hm.
+ clear e0;inversion_clear Hm.
  assert (notin:~ In y (remove x l)) by auto.
  intros (x1,abs).
  inversion_clear abs. 
@@ -393,7 +391,7 @@ Proof.
 
 
  assert (cmp_e_e':cmp e e' = true).
-  apply H2 with x; auto.
+  apply H1 with x; auto.
  rewrite cmp_e_e'; simpl.
  apply IHb; auto.
  inversion_clear Hm; auto.
@@ -402,7 +400,7 @@ Proof.
  destruct (H0 k).
  assert (In k ((x,e) ::l)).
   destruct H as (e'', hyp); exists e''; auto.
- destruct (In_inv (H1 H4)); auto.
+ destruct (In_inv (H2 H4)); auto.
  inversion_clear Hm.
  elim (Sort_Inf_NotIn H6 H7).
  destruct H as (e'', hyp); exists e''; auto.
@@ -415,10 +413,10 @@ Proof.
  elim (Sort_Inf_NotIn H6 H7).
  destruct H as (e'', hyp); exists e''; auto.
  apply MapsTo_eq with k; auto; order.
- apply H2 with k; destruct (eq_dec x k); auto.
+ apply H1 with k; destruct (eq_dec x k); auto.
 
 
- destruct (X.compare x x'); try contradiction;clear H2.
+ destruct (X.compare x x'); try contradiction; clear y.
  destruct (H0 x).
  assert (In x ((x',e')::l')). 
   apply H; auto.
@@ -492,16 +490,16 @@ Proof.
 
  inversion_clear Hm;inversion_clear Hm'.
  destruct (andb_prop _ _ H); clear H. 
- destruct (IHb H1 H4 H7).
+ destruct (IHb H2 H4 H7).
  inversion_clear H0.
  destruct H9; simpl in *; subst.
- inversion_clear H2. 
+ inversion_clear H1. 
  destruct H9; simpl in *; subst; auto.
  elim (Sort_Inf_NotIn H4 H5).
  exists e'0; apply MapsTo_eq with k; auto; order.
- inversion_clear H2. 
+ inversion_clear H1. 
  destruct H0; simpl in *; subst; auto.
- elim (Sort_Inf_NotIn H1 H3).
+ elim (Sort_Inf_NotIn H2 H3).
  exists e0; apply MapsTo_eq with k; auto; order.
  apply H8 with k; auto.
 Qed. 
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 3a91b868..890485a8 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FMapWeakList.v 8899 2006-06-06 11:09:43Z jforest $ *)
+(* $Id: FMapWeakList.v 8985 2006-06-23 16:12:45Z jforest $ *)
 
 (** * Finite map library *)  
 
@@ -104,8 +104,8 @@ Proof.
  inversion belong1. inversion H.
  inversion_clear NoDup.
  inversion_clear belong1.
- inversion_clear H2.
- compute in H3; destruct H3.
+ inversion_clear H1.
+ compute in H2; destruct H2.
  contradiction.
  apply IHb; auto.
  exists x0; auto.
@@ -144,11 +144,11 @@ Proof.
  inversion 2.
 
  do 2 inversion_clear 1.
- compute in H3; destruct H3; subst; trivial.
+ compute in H2; destruct H2; subst; trivial.
  elim H; apply InA_eqk with (x,e); auto.
 
  do 2 inversion_clear 1; auto.
- compute in H3; destruct H3; elim _x; auto.
+ compute in H2; destruct H2; elim _x; auto.
 Qed.
 
 (* Not part of the exported specifications, used later for [combine]. *)
@@ -184,7 +184,7 @@ Proof.
  intros m x  y e e'; generalize y e; clear y e; unfold PX.MapsTo.
  functional induction (add x e' m);simpl;auto.
  intros y' e'' eqky';  inversion_clear 1.
- destruct H1; simpl in *.
+ destruct H0; simpl in *.
  elim eqky'; apply X.eq_trans with k'; auto.
  auto.
  intros y' e'' eqky'; inversion_clear 1; intuition.
@@ -196,7 +196,7 @@ Proof.
  intros m x y e e'. generalize y e; clear y e; unfold PX.MapsTo.
  functional induction (add x e' m);simpl;auto.
  intros; apply (In_inv_3 H0); auto.
- constructor 2; apply (In_inv_3 H1); auto.
+ constructor 2; apply (In_inv_3 H0); auto.
  inversion_clear 2; auto.
 Qed.
 
@@ -208,8 +208,8 @@ Proof.
  inversion_clear 2.
  compute in H1; elim H; auto.
  inversion H1. 
- constructor 2; inversion_clear H1; auto.
- compute in H2; elim H; auto.
+ constructor 2; inversion_clear H0; auto.
+ compute in H1; elim H; auto.
  inversion_clear 2; auto.
 Qed.
 
@@ -272,17 +272,17 @@ Proof.
 
  inversion_clear Hm.
  subst.
- swap H1.
- destruct H3 as (e,H3); unfold PX.MapsTo in H3.
+ swap H0.
+ destruct H2 as (e,H2); unfold PX.MapsTo in H2.
  apply InA_eqk with (y,e); auto.
  compute; apply X.eq_trans with x; auto.
   
  intro H2.
  destruct H2 as (e,H2); inversion_clear H2.
- compute in H1; destruct H1.
+ compute in H0; destruct H0.
  elim _x; apply X.eq_trans with y; auto.
  inversion_clear Hm.
- elim (IHt0 H3 H).
+ elim (IHt0 H2 H).
  exists e; auto.
 Qed.
   
@@ -292,7 +292,7 @@ Proof.
  intros m Hm x y e; generalize Hm; clear Hm; unfold PX.MapsTo.
  functional induction (remove x m);auto.
  inversion_clear 3; auto.
- compute in H2; destruct H2.
+ compute in H1; destruct H1.
  elim H; apply X.eq_trans with k'; auto.
   
  inversion_clear 1; inversion_clear 2; auto.
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index b385f50e..5b09945b 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -12,7 +12,7 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: FSetAVL.v 8899 2006-06-06 11:09:43Z jforest $ *)
+(* $Id: FSetAVL.v 8985 2006-06-23 16:12:45Z jforest $ *)
 
 (** This module implements sets using AVL trees.
     It follows the implementation from Ocaml's standard library. *)
@@ -515,7 +515,7 @@ Proof.
  (* LT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt y0 H1); intuition_in.
+ rewrite (IHt y0 H0); intuition_in.
  (* EQ *)  
  inv avl.
  intuition.
@@ -523,7 +523,7 @@ Proof.
  (* GT *)
  inv avl.
  rewrite bal_in; auto.
- rewrite (IHt y0 H2); intuition_in.
+ rewrite (IHt y0 H1); intuition_in.
 Qed.
 
 Lemma add_bst : forall s x, bst s -> avl s -> bst (add x s).
@@ -531,16 +531,16 @@ Proof.
  intros s x; functional induction (add x s); auto; intros.
  inv bst; inv avl; apply bal_bst; auto.
  (* lt_tree -> lt_tree (add ...) *)
- red; red in H5.
+ red; red in H4.
  intros.
- rewrite (add_in l x y0 H) in H1.
+ rewrite (add_in l x y0 H) in H0.
  intuition.
  eauto.
  inv bst; inv avl; apply bal_bst; auto.
  (* gt_tree -> gt_tree (add ...) *)
- red; red in H5.
+ red; red in H4.
  intros.
- rewrite (add_in r x y0 H6) in H1.
+ rewrite (add_in r x y0 H5) in H0.
  intuition.
  apply MX.lt_eq with x; auto.
 Qed.
@@ -703,7 +703,7 @@ Proof.
  avl_nns; omega_max.
  (* l = Node *)
  inversion_clear H.
- rewrite H0 in IHp;simpl in IHp;destruct (IHp lh); auto.
+ rewrite e0 in IHp;simpl in IHp;destruct (IHp lh); auto.
  split; simpl in *. 
  apply bal_avl; auto; omega_max.
  omega_bal.
@@ -723,12 +723,12 @@ Proof.
  intuition_in.
  (* l = Node *)
  inversion_clear H.
- generalize (remove_min_avl ll lx lr lh H1).
- rewrite H0; simpl; intros.
+ generalize (remove_min_avl ll lx lr lh H0).
+ rewrite e0; simpl; intros.
  rewrite bal_in; auto.
- rewrite H0 in IHp;generalize (IHp lh y H1).
+ rewrite e0 in IHp;generalize (IHp lh y H0).
  intuition.
- inversion_clear H8; intuition.
+ inversion_clear H7; intuition.
 Qed.
 
 Lemma remove_min_bst : forall l x r h, 
@@ -736,15 +736,15 @@ Lemma remove_min_bst : forall l x r h,
 Proof.
  intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros.
  inv bst; auto.
- inversion_clear H; inversion_clear H1.
- rewrite_all H0;simpl in *.
+ inversion_clear H; inversion_clear H0.
+ rewrite_all e0;simpl in *.
  apply bal_bst; auto.
  firstorder.
  intro; intros.
  generalize (remove_min_in ll lx lr lh y H).
- rewrite H0; simpl.
+ rewrite e0; simpl.
  destruct 1.
- apply H4; intuition.
+ apply H3; intuition.
 Qed.
 
 Lemma remove_min_gt_tree : forall l x r h, 
@@ -753,14 +753,14 @@ Lemma remove_min_gt_tree : forall l x r h,
 Proof.
  intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros.
  inv bst; auto.
- inversion_clear H; inversion_clear H1.
+ inversion_clear H; inversion_clear H0.
  intro; intro.
- generalize (IHp lh H2 H); clear H8 H7 IHp.
+ generalize (IHp lh H1 H); clear H6 H7 IHp.
  generalize (remove_min_avl ll lx lr lh H).
  generalize (remove_min_in ll lx lr lh m H).
- rewrite H0; simpl; intros.
- rewrite (bal_in l' x r y H8 H6) in H1.
- destruct H7.
+ rewrite e0; simpl; intros.
+ rewrite (bal_in l' x r y H7 H5) in H0.
+ destruct H6.
  firstorder.
  apply MX.lt_eq with x; auto.
  apply X.lt_trans with x; auto.
@@ -788,9 +788,9 @@ Proof.
  intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros.
  split; auto; avl_nns; omega_max.
  split; auto; avl_nns; simpl in *; omega_max.
- destruct s1;try contradiction;clear H1.
+ destruct s1;try contradiction;clear y.
  generalize (remove_min_avl_1 l2 x2 r2 h2 H0).
- rewrite H2; simpl; destruct 1.
+ rewrite e1; simpl; destruct 1.
  split.
  apply bal_avl; auto.
  simpl; omega_max.
@@ -809,12 +809,12 @@ Proof.
  intros s1 s2; functional induction (merge s1 s2); subst; simpl in *; intros.
  intuition_in.
  intuition_in.
- destruct s1;try contradiction;clear H1.
- replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite H2; auto].
+ destruct s1;try contradiction;clear y.
+ replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite e1; auto].
  rewrite bal_in; auto.
- generalize (remove_min_avl l2 x2 r2 h2); rewrite H2; simpl; auto.
- generalize (remove_min_in l2 x2 r2 h2 y); rewrite H2; simpl; intro.
- rewrite H1; intuition.
+ generalize (remove_min_avl l2 x2 r2 h2); rewrite e1; simpl; auto.
+ generalize (remove_min_in l2 x2 r2 h2 y0); rewrite e1; simpl; intro.
+ rewrite H3 ; intuition.
 Qed.
 
 Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
@@ -822,13 +822,13 @@ Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 ->
  bst (merge s1 s2). 
 Proof.
  intros s1 s2; functional induction (merge s1 s2); subst;simpl in *; intros; auto.
- destruct s1;try contradiction;clear H1.
+ destruct s1;try contradiction;clear y.
  apply bal_bst; auto.
- generalize (remove_min_bst l2 x2 r2 h2); rewrite H2; simpl in *; auto.
+ generalize (remove_min_bst l2 x2 r2 h2); rewrite e1; simpl in *; auto.
  intro; intro.
- apply H5; auto.
- generalize (remove_min_in l2 x2 r2 h2 m); rewrite H2; simpl; intuition.
- generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite H2; simpl; auto.
+ apply H3; auto.
+ generalize (remove_min_in l2 x2 r2 h2 m); rewrite e1; simpl; intuition.
+ generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite e1; simpl; auto.
 Qed. 
 
 (** * Deletion *)
@@ -850,18 +850,18 @@ Proof.
  intuition; omega_max.
  (* LT *)
  inv avl.
- destruct (IHt H1).
+ destruct (IHt H0).
  split. 
  apply bal_avl; auto.
  omega_max.
  omega_bal.
  (* EQ *)
  inv avl. 
- generalize (merge_avl_1 l r H1 H2 H3).
+ generalize (merge_avl_1 l r H0 H1 H2).
  intuition omega_max.
  (* GT *)
  inv avl.
- destruct (IHt H2).
+ destruct (IHt H1).
  split. 
  apply bal_avl; auto.
  omega_max.
@@ -880,17 +880,17 @@ Proof.
  intros s x; functional induction (remove x s); subst;simpl; intros.
  intuition_in.
  (* LT *)
- inv avl; inv bst; clear H0.
+ inv avl; inv bst; clear e0.
  rewrite bal_in; auto.
- generalize (IHt y0 H1); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H0); intuition; [ order | order | intuition_in ].
  (* EQ *)
- inv avl; inv bst; clear H0.
+ inv avl; inv bst; clear e0.
  rewrite merge_in; intuition; [ order | order | intuition_in ].
  elim H9; eauto.
  (* GT *)
- inv avl; inv bst; clear H0.
+ inv avl; inv bst; clear e0.
  rewrite bal_in; auto.
- generalize (IHt y0 H6); intuition; [ order | order | intuition_in ].
+ generalize (IHt y0 H5); intuition; [ order | order | intuition_in ].
 Qed.
 
 Lemma remove_bst : forall s x, bst s -> avl s -> bst (remove x s).
@@ -945,7 +945,7 @@ Proof.
  simpl.
  destruct l1.
  inversion 1; subst.
- assert (X.lt x _x) by (apply H3; auto).
+ assert (X.lt x _x) by (apply H2; auto).
  inversion_clear 1; auto; order.
  assert (X.lt t _x) by auto.
  inversion_clear 2; auto; 
@@ -958,7 +958,7 @@ Proof.
  red; auto.
  inversion 1.
  destruct l;try contradiction. 
- clear H0;intro H0.
+ clear y;intro H0.
  destruct (IHo H0 t);  auto.
 Qed.
 
@@ -1004,7 +1004,7 @@ Proof.
  red; auto.
  inversion 1.
  destruct r;try contradiction.
- clear H0;intros H0; destruct (IHo H0 t); auto.
+ intros H0; destruct (IHo H0 t); auto.
 Qed.
 
 (** * Any element *)
@@ -1038,9 +1038,9 @@ Function concat (s1 s2 : t) : t  :=
 Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2).
 Proof.
  intros s1 s2; functional induction (concat s1 s2); subst;auto.
- destruct s1;try contradiction;clear H1.
+ destruct s1;try contradiction;clear y.
  intros; apply join_avl; auto.
- generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite H2; simpl; auto.
+ generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite e1; simpl; auto.
 Qed.
  
 Lemma concat_bst :   forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
@@ -1048,13 +1048,13 @@ Lemma concat_bst :   forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 ->
  bst (concat s1 s2).
 Proof. 
  intros s1 s2; functional induction (concat s1 s2); subst ;auto.
- destruct s1;try contradiction;clear H1. 
+ destruct s1;try contradiction;clear y. 
  intros;  apply join_bst; auto.
- generalize (remove_min_bst l2 x2 r2 h2 H1 H3); rewrite H2; simpl; auto.
- generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto.
- generalize (remove_min_in l2 x2 r2 h2 m H3); rewrite H2; simpl; auto.
+ generalize (remove_min_bst l2 x2 r2 h2 H1 H2); rewrite e1; simpl; auto.
+ generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite e1; simpl; auto.
+ generalize (remove_min_in l2 x2 r2 h2 m H2); rewrite e1; simpl; auto.
  destruct 1; intuition.
- generalize (remove_min_gt_tree l2 x2 r2 h2 H1 H3); rewrite H2; simpl; auto.
+ generalize (remove_min_gt_tree l2 x2 r2 h2 H1 H2); rewrite e1; simpl; auto.
 Qed.
 
 Lemma concat_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
@@ -1064,12 +1064,12 @@ Proof.
  intros s1 s2; functional induction (concat s1 s2);subst;simpl.
  intuition.
  inversion_clear H5.
- destruct s1;try contradiction;clear H1;intuition.
+ destruct s1;try contradiction;clear y;intuition.
  inversion_clear H5.
- destruct s1;try contradiction;clear H1; intros. 
+ destruct s1;try contradiction;clear y; intros. 
  rewrite (join_in  (Node s1_1 t s1_2 i) m s2' y H0).
- generalize (remove_min_avl l2 x2 r2 h2 H3); rewrite H2; simpl; auto.
- generalize (remove_min_in l2 x2 r2 h2 y H3); rewrite H2; simpl.
+ generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite e1; simpl; auto.
+ generalize (remove_min_in l2 x2 r2 h2 y H2); rewrite e1; simpl.
  intro EQ; rewrite EQ; intuition.
 Qed.
 
@@ -1100,9 +1100,9 @@ Lemma split_avl : forall s x, avl s ->
 Proof. 
  intros s x; functional induction (split x s);subst;simpl in *.
  auto.
- rewrite H1 in IHp;simpl in IHp;inversion_clear 1; intuition.
+ rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition.
  simpl; inversion_clear 1; auto.
- rewrite H1 in IHp;simpl in IHp;inversion_clear 1; intuition.
+ rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition.
 Qed.
 
 Lemma split_in_1 : forall s x y, bst s -> avl s -> 
@@ -1111,20 +1111,20 @@ Proof.
  intros s x; functional induction (split x s);subst;simpl in *.
  intuition; try inversion_clear H1.
  (* LT *)
- rewrite H1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear  H8 H9.
- rewrite (IHp y0 H2 H6); clear IHp H0.
+ rewrite e1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear  H7 H6.
+ rewrite (IHp y0 H0 H4); clear IHp e0.
  intuition.
- inversion_clear H0; auto; order.
+ inversion_clear H6; auto; order.
  (* EQ *)
- simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H7 H0.
+ simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0.
  intuition.
  order.
  intuition_in; order.
  (* GT *)
- rewrite H1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8.
+ rewrite e1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
  rewrite join_in; auto.
- generalize (split_avl r x H7); rewrite H1; simpl; intuition.
- rewrite (IHp y0 H3 H7); clear H1.
+ generalize (split_avl r x H5); rewrite e1; simpl; intuition.
+ rewrite (IHp y0 H1 H5); clear e1.
  intuition; [ eauto | eauto | intuition_in ].
 Qed.
 
@@ -1134,17 +1134,17 @@ Proof.
  intros s x; functional induction (split x s);subst;simpl in *.
  intuition; try inversion_clear H1.
  (* LT *)
- rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8.
+ rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
   rewrite join_in; auto.
- generalize (split_avl l x H6); rewrite H1; simpl; intuition.
- rewrite (IHp y0 H2 H6); clear IHp H0.
+ generalize (split_avl l x H4); rewrite e1; simpl; intuition.
+ rewrite (IHp y0 H0 H4); clear IHp e0.
  intuition; [ order | order | intuition_in ].
  (* EQ *)
- simpl in *; inversion_clear 1; inversion_clear 1; clear H8 H7 H0.
+ simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0.
  intuition; [ order | intuition_in; order ]. 
  (* GT *)
- rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8.
- rewrite (IHp y0 H3 H7); clear IHp H0.
+ rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
+ rewrite (IHp y0 H1 H5); clear IHp e0.
  intuition; intuition_in; order. 
 Qed.
 
@@ -1154,13 +1154,13 @@ Proof.
  intros s x; functional induction (split x s);subst;simpl in *.
  intuition; try inversion_clear H1.
  (* LT *)
- rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8.
+ rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
  rewrite IHp; auto.
  intuition_in; absurd (X.lt x y); eauto.
  (* EQ *)
  simpl in *; inversion_clear 1; inversion_clear 1; intuition.
  (* GT *)
- rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H9 H8.
+ rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
  rewrite IHp; auto.
  intuition_in; absurd (X.lt y x); eauto.
 Qed.
@@ -1171,21 +1171,21 @@ Proof.
  intros s x; functional induction (split x s);subst;simpl in *.  
  intuition.
  (* LT *)
- rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1.
+ rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1.
  intuition.
  apply join_bst; auto.
- generalize (split_avl l x H6); rewrite H1; simpl; intuition.
+ generalize (split_avl l x H4); rewrite e1; simpl; intuition.
  intro; intro.
- generalize (split_in_2 l x y0 H2 H6); rewrite H1; simpl; intuition.
+ generalize (split_in_2 l x y0 H0 H4); rewrite e1; simpl; intuition.
  (* EQ *)
  simpl in *; inversion_clear 1; inversion_clear 1; intuition.
  (* GT *)
- rewrite H1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1.
+ rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1.
  intuition.
  apply join_bst; auto.
- generalize (split_avl r x H7); rewrite H1; simpl; intuition.
+ generalize (split_avl r x H5); rewrite e1; simpl; intuition.
  intro; intro.
- generalize (split_in_1 r x y0 H3 H7); rewrite H1; simpl; intuition.
+ generalize (split_in_1 r x y0 H1 H5); rewrite e1; simpl; intuition.
 Qed.
 
 (** * Intersection *)
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index fde70225..4e0f3745 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Wf.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Wf.v 8988 2006-06-25 22:15:32Z letouzey $ i*)
 
 (** This module proves the validity of
     - well-founded recursion (also called course of values)
@@ -146,6 +146,8 @@ Section Well_founded_2.
   Variable R : A * B -> A * B -> Prop.
 
   Variable P : A -> B -> Type. 
+
+  Section Acc_iter_2.
   Variable
     F :
       forall (x:A) (x':B),
@@ -156,6 +158,7 @@ Section Well_founded_2.
     F
       (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
          Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)).
+  End Acc_iter_2.
 
   Hypothesis Rwf : well_founded R.
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 751bc3da..df2b17e0 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -6,7 +6,7 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id: List.v 8866 2006-05-28 16:21:04Z herbelin $ i*)
+  (*i $Id: List.v 9035 2006-07-09 15:42:09Z herbelin $ i*)
 
 Require Import Le Gt Minus Min Bool.
 Require Import Setoid.
@@ -85,6 +85,7 @@ Delimit Scope list_scope with list.
 
 Bind Scope list_scope with list.
 
+Arguments Scope list [type_scope].
 
 (** ** Facts about lists *)
 
@@ -135,13 +136,11 @@ Section Facts.
   Proof. 
     simpl in |- *; auto.
   Qed.
-  Hint Resolve in_eq.
   
   Theorem in_cons : forall (a b:A) (l:list A), In b l -> In b (a :: l).
   Proof. 
     simpl in |- *; auto.
   Qed.
-  Hint Resolve in_cons.
 
   Theorem in_nil : forall a:A, ~ In a nil.
   Proof.
@@ -197,8 +196,6 @@ Section Facts.
     induction l; simpl in |- *; auto.
     rewrite <- IHl; auto.
   Qed.
-  Hint Resolve app_nil_end.
-  
 
   (** [app] is associative *)
   Theorem app_ass : forall l m n:list A, (l ++ m) ++ n = l ++ m ++ n.
@@ -211,9 +208,8 @@ Section Facts.
 
   Theorem ass_app : forall l m n:list A, l ++ m ++ n = (l ++ m) ++ n.
   Proof. 
-    auto.
+    auto using app_ass.
   Qed.
-  Hint Resolve ass_app.
 
   (** [app] commutes with [cons] *) 
   Theorem app_comm_cons : forall (x y:list A) (a:A), a :: (x ++ y) = (a :: x) ++ y.
@@ -296,7 +292,6 @@ Section Facts.
     now_show ((a0 = a \/ In a y) \/ In a m).
     elim (H H1); auto.
   Qed.
-  Hint Immediate in_app_or.
 
   Lemma in_or_app : forall (l m:list A) (a:A), In a l \/ In a m -> In a (l ++ m).
   Proof. 
@@ -313,7 +308,6 @@ Section Facts.
     now_show (H = a \/ In a (y ++ m)).
     elim H2; auto.
   Qed.
-  Hint Resolve in_or_app.
 
 
 End Facts.
@@ -890,7 +884,7 @@ Section ListOps.
     break_list l1 b l1' H0; break_list l3 c l3' H1.
     auto.
     apply perm_trans with (l3'++c::l4); auto.
-    apply perm_trans with (l1'++a::l2); auto.
+    apply perm_trans with (l1'++a::l2); auto using Permutation_cons_app.
     apply perm_skip.
     apply (IH a l1' l2 l3' l4); auto.
     (* swap *)
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index e0be9ed3..d2b7db04 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ChoiceFacts.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
+(*i $Id: ChoiceFacts.v 8999 2006-07-04 12:46:04Z notin $ i*)
 
 (** ** Some facts and definitions concerning choice and description in
        intuitionistic logic.
@@ -78,7 +78,7 @@ unpublished.
 [Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic
 Type Theories, Mathematical Logic Quarterly, volume 39, 1993.
 
-[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in
+[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in
 intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
 *)
 
@@ -125,7 +125,7 @@ Definition FunctionalRelReification_on :=
 
 (** ID_epsilon (constructive version of indefinite description;
     combined with proof-irrelevance, it may be connected to
-    Carlstrøm's type theory with a constructive indefinite description
+    Carlstrøm's type theory with a constructive indefinite description
     operator) *)
 
 Definition ConstructiveIndefiniteDescription_on :=
@@ -133,7 +133,7 @@ Definition ConstructiveIndefiniteDescription_on :=
   (exists x, P x) -> { x:A | P x }.
 
 (** ID_iota (constructive version of definite description; combined
-    with proof-irrelevance, it may be connected to Carlstrøm's and
+    with proof-irrelevance, it may be connected to Carlstrøm's and
     Stenlund's type theory with a constructive definite description
     operator) *)
 
@@ -694,7 +694,7 @@ Qed.
     We adapt the proof to show that constructive definite description
     transports excluded-middle from [Prop] to [Set].
 
-    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
     Simpson, Mathematical Quotients and Quotient Types in Coq,
     Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
     Springer Verlag.  *)
diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index 79bef2af..28d32fcc 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalUniqueChoice.v 8893 2006-06-04 18:04:53Z herbelin $ i*)
+(*i $Id: ClassicalUniqueChoice.v 9026 2006-07-06 15:16:20Z herbelin $ i*)
 
 (** This file provides classical logic and unique choice *)
 
@@ -15,7 +15,7 @@
     excluded-middle in [Set], hence it implies a strongly classical
     world. Especially it conflicts with the impredicativity of [Set].
 
-    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
     Simpson, Mathematical Quotients and Quotient Types in Coq,
     Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
     Springer Verlag.  *)
@@ -39,7 +39,7 @@ intros A B.
 apply (dependent_unique_choice A (fun _ => B)).
 Qed.
 
-(** The followig proof comes from [ChicliPottierSimpson02] *)
+(** The following proof comes from [ChicliPottierSimpson02] *)
 
 Require Import Setoid.
 
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 1d56b747..335466a6 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: QArith_base.v 8883 2006-05-31 21:56:37Z letouzey $ i*)
+(*i $Id: QArith_base.v 8989 2006-06-25 22:17:49Z letouzey $ i*)
 
 Require Export ZArith.
 Require Export ZArithRing.
@@ -43,12 +43,48 @@ Notation Qge := (fun x y : Q => Qle y x).
 
 Infix "==" := Qeq (at level 70, no associativity) : Q_scope. 
 Infix "<" := Qlt : Q_scope.
+Infix ">" := Qgt : Q_scope.
 Infix "<=" := Qle : Q_scope.
-Infix ">" := Qgt : Q_scope. 
-Infix ">=" := Qge : Q_scope. 
+Infix ">=" := Qge : Q_scope.
 Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope.
 
-Hint Unfold Qeq Qle Qlt: qarith.
+(** Another approach : using Qcompare for defining order relations. *)
+
+Definition Qcompare (p q : Q) := (Qnum p * QDen q ?= Qnum q * QDen p)%Z.
+Notation "p ?= q" := (Qcompare p q) : Q_scope.
+
+Lemma Qeq_alt : forall p q, (p == q) <-> (p ?= q) = Eq.
+Proof.
+unfold Qeq, Qcompare; intros; split; intros.
+rewrite H; apply Zcompare_refl.
+apply Zcompare_Eq_eq; auto.
+Qed.
+
+Lemma Qlt_alt : forall p q, (p<q) <-> (p?=q = Lt).
+Proof.
+unfold Qlt, Qcompare, Zlt; split; auto.
+Qed.
+
+Lemma Qgt_alt : forall p q, (p>q) <-> (p?=q = Gt).
+Proof.
+unfold Qlt, Qcompare, Zlt.
+intros; rewrite Zcompare_Gt_Lt_antisym; split; auto.
+Qed.
+
+Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt).
+Proof.
+unfold Qle, Qcompare, Zle; split; auto.
+Qed.
+
+Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt).
+Proof.
+unfold Qle, Qcompare, Zle.
+split; intros; swap H.
+rewrite Zcompare_Gt_Lt_antisym; auto.
+rewrite Zcompare_Gt_Lt_antisym in H0; auto.
+Qed.
+
+Hint Unfold Qeq Qlt Qle: qarith.
 Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith.
 
 (** Properties of equality. *)
@@ -236,6 +272,24 @@ apply Zmult_gt_0_lt_compat_l; auto with zarith.
 Open Scope Q_scope.
 Qed.
 
+
+Lemma Qcompare_egal_dec: forall n m p q : Q, 
+ (n<m -> p<q) -> (n==m -> p==q) -> (n>m -> p>q) -> ((n?=m) = (p?=q)).
+Proof.
+intros.
+do 2 rewrite Qeq_alt in H0.
+unfold Qeq, Qlt, Qcompare in *.
+apply Zcompare_egal_dec; auto.
+omega.
+Qed.
+
+
+Add Morphism Qcompare : Qcompare_comp.
+Proof.
+intros; apply Qcompare_egal_dec; rewrite H; rewrite H0; auto.
+Qed.
+
+
 (** [0] and [1] are apart *)
 
 Lemma Q_apart_0_1 : ~ 1 == 0.
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
new file mode 100644
index 00000000..9cbd400d
--- /dev/null
+++ b/theories/QArith/Qcanon.v
@@ -0,0 +1,526 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Qcanon.v 8989 2006-06-25 22:17:49Z letouzey $ i*)
+
+Require Import QArith.
+Require Import Eqdep_dec.
+
+(** [Qc] : A canonical representation of rational numbers. 
+   based on the setoid representation [Q]. *)
+
+Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }.
+
+Delimit Scope Qc_scope with Qc.
+Bind Scope Qc_scope with Qc.
+Arguments Scope Qcmake [Q_scope].
+Open Scope Qc_scope.
+
+Lemma Qred_identity : 
+ forall q:Q, Zgcd (Qnum q) (QDen q) = 1%Z -> Qred q = q.
+Proof.
+unfold Qred; intros (a,b); simpl.
+generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)).
+intros.
+rewrite H1 in H; clear H1.
+destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
+destruct H0.
+rewrite Zmult_1_l in H, H0.
+subst; simpl; auto.
+Qed.
+
+Lemma Qred_identity2 : 
+ forall q:Q, Qred q = q -> Zgcd (Qnum q) (QDen q) = 1%Z.
+Proof.
+unfold Qred; intros (a,b); simpl.
+generalize (Zggcd_gcd a ('b)) (Zggcd_correct_divisors a ('b)) (Zgcd_is_pos a ('b)).
+intros.
+rewrite <- H; rewrite <- H in H1; clear H.
+destruct (Zggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
+injection H2; intros; clear H2.
+destruct H0.
+clear H0 H3.
+destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate.
+f_equal.
+apply Pmult_reg_r with bb.
+injection H2; intros. 
+rewrite <- H0.
+rewrite H; simpl; auto.
+elim H1; auto.
+Qed.
+
+Lemma Qred_iff : forall q:Q, Qred q = q <-> Zgcd (Qnum q) (QDen q) = 1%Z.
+Proof.
+split; intros.
+apply Qred_identity2; auto.
+apply Qred_identity; auto.
+Qed.
+
+
+Lemma Qred_involutive : forall q:Q, Qred (Qred q) = Qred q.
+Proof.
+intros; apply Qred_complete.
+apply Qred_correct.
+Qed.
+
+Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). 
+Arguments Scope Q2Qc [Q_scope].
+Notation " !! " := Q2Qc : Qc_scope.
+
+Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'.
+Proof.
+intros (q,proof_q) (q',proof_q').
+simpl.
+intros H.
+assert (H0:=Qred_complete _ _ H).
+assert (q = q') by congruence.
+subst q'.
+assert (proof_q = proof_q'). 
+ apply eq_proofs_unicity; auto; intros.
+ repeat decide equality.
+congruence.
+Qed.
+Hint Resolve Qc_is_canon.
+
+Notation " 0 " := (!!0) : Qc_scope.
+Notation " 1 " := (!!1) : Qc_scope.
+
+Definition Qcle (x y : Qc) := (x <= y)%Q.
+Definition Qclt (x y : Qc) := (x < y)%Q.
+Notation Qcgt := (fun x y : Qc => Qlt y x).
+Notation Qcge := (fun x y : Qc => Qle y x).
+Infix "<" := Qclt : Qc_scope.
+Infix "<=" := Qcle : Qc_scope.
+Infix ">" := Qcgt : Qc_scope. 
+Infix ">=" := Qcge : Qc_scope. 
+Notation "x <= y <= z" := (x<=y/\y<=z) : Qc_scope.
+
+Definition Qccompare (p q : Qc) := (Qcompare p q).
+Notation "p ?= q" := (Qccompare p q) : Qc_scope.
+
+Lemma Qceq_alt : forall p q, (p = q) <-> (p ?= q) = Eq.
+Proof.
+unfold Qccompare.
+intros; rewrite <- Qeq_alt.
+split; auto.
+intro H; rewrite H; auto with qarith.
+Qed.
+
+Lemma Qclt_alt : forall p q, (p<q) <-> (p?=q = Lt).
+Proof.
+intros; exact (Qlt_alt p q).
+Qed.
+
+Lemma Qcgt_alt : forall p q, (p>q) <-> (p?=q = Gt).
+Proof.
+intros; exact (Qgt_alt p q).
+Qed.
+
+Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt).
+Proof.
+intros; exact (Qle_alt p q).
+Qed.
+
+Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt).
+Proof.
+intros; exact (Qge_alt p q).
+Qed.
+
+(** equality on [Qc] is decidable: *)
+
+Theorem Qc_eq_dec : forall x y:Qc, {x=y} + {x<>y}.
+Proof.
+ intros.
+ destruct (Qeq_dec x y) as [H|H]; auto.
+ right; swap H; subst; auto with qarith.
+Defined. 
+
+(** The addition, multiplication and opposite are defined 
+   in the straightforward way: *)
+
+Definition Qcplus (x y : Qc) := !!(x+y).
+Infix "+" := Qcplus : Qc_scope.
+Definition Qcmult (x y : Qc) := !!(x*y).
+Infix "*" := Qcmult : Qc_scope.
+Definition Qcopp (x : Qc) := !!(-x).
+Notation "- x" := (Qcopp x) : Qc_scope.
+Definition Qcminus (x y : Qc) := x+-y.
+Infix "-" := Qcminus : Qc_scope.
+Definition Qcinv (x : Qc) := !!(/x).
+Notation "/ x" := (Qcinv x) : Qc_scope. 
+Definition Qcdiv (x y : Qc) := x*/y.
+Infix "/" := Qcdiv : Qc_scope. 
+
+(** [0] and [1] are apart *)
+
+Lemma Q_apart_0_1 : 1 <> 0.
+Proof.
+ unfold Q2Qc.
+ intros H; discriminate H.
+Qed.
+
+Ltac qc := match goal with 
+ | q:Qc |- _ => destruct q; qc 
+ | _ => apply Qc_is_canon; simpl; repeat rewrite Qred_correct
+end.
+
+Opaque Qred.
+
+(** Addition is associative: *)
+
+Theorem Qcplus_assoc : forall x y z, x+(y+z)=(x+y)+z.
+Proof.
+ intros; qc; apply Qplus_assoc.
+Qed.
+
+(** [0] is a neutral element for addition: *)
+
+Lemma Qcplus_0_l : forall x, 0+x = x.
+Proof.
+ intros; qc; apply Qplus_0_l.
+Qed.
+
+Lemma Qcplus_0_r : forall x, x+0 = x.
+Proof.
+ intros; qc; apply Qplus_0_r.
+Qed. 
+
+(** Commutativity of addition: *)
+
+Theorem Qcplus_comm : forall x y, x+y = y+x.
+Proof.
+ intros; qc; apply Qplus_comm.
+Qed.
+
+(** Properties of [Qopp] *)
+
+Lemma Qcopp_involutive : forall q, - -q = q.
+Proof.
+ intros; qc; apply Qopp_involutive.
+Qed.
+
+Theorem Qcplus_opp_r : forall q, q+(-q) = 0.
+Proof.
+ intros; qc; apply Qplus_opp_r.
+Qed.
+
+(** Multiplication is associative: *)
+
+Theorem Qcmult_assoc : forall n m p, n*(m*p)=(n*m)*p.
+Proof.
+ intros; qc; apply Qmult_assoc.
+Qed.
+
+(** [1] is a neutral element for multiplication: *)
+
+Lemma Qcmult_1_l : forall n, 1*n = n.
+Proof.
+ intros; qc; apply Qmult_1_l.
+Qed.
+
+Theorem Qcmult_1_r : forall n, n*1=n.
+Proof.
+ intros; qc; apply Qmult_1_r.
+Qed.
+
+(** Commutativity of multiplication *)
+
+Theorem Qcmult_comm : forall x y, x*y=y*x.
+Proof.
+ intros; qc; apply Qmult_comm.
+Qed.
+
+(** Distributivity *)
+
+Theorem Qcmult_plus_distr_r : forall x y z, x*(y+z)=(x*y)+(x*z).
+Proof.
+ intros; qc; apply Qmult_plus_distr_r.
+Qed.
+
+Theorem Qcmult_plus_distr_l : forall x y z, (x+y)*z=(x*z)+(y*z).
+Proof.
+ intros; qc; apply Qmult_plus_distr_l.
+Qed.
+
+(** Integrality *)
+
+Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0.
+Proof.
+ intros.
+ destruct (Qmult_integral x y); try qc; auto.
+ injection H; clear H; intros.
+ rewrite <- (Qred_correct (x*y)).
+ rewrite <- (Qred_correct 0).
+ rewrite H; auto with qarith.
+Qed.
+
+Theorem Qcmult_integral_l : forall x y, ~ x = 0 -> x*y = 0 -> y = 0.
+Proof.
+ intros; destruct (Qcmult_integral _ _ H0); tauto.
+Qed. 
+
+(** Inverse and division. *) 
+
+Theorem Qcmult_inv_r : forall x, x<>0 -> x*(/x) = 1.
+Proof.
+ intros; qc; apply Qmult_inv_r; auto. 
+Qed.
+
+Theorem Qcmult_inv_l : forall x, x<>0 -> (/x)*x = 1.
+Proof.
+ intros.
+ rewrite Qcmult_comm.
+ apply Qcmult_inv_r; auto.
+Qed.
+
+Lemma Qcinv_mult_distr : forall p q, / (p * q) = /p * /q.
+Proof.
+ intros; qc; apply Qinv_mult_distr.
+Qed.
+
+Theorem Qcdiv_mult_l : forall x y, y<>0 -> (x*y)/y = x.
+Proof.
+ unfold Qcdiv.
+ intros.
+ rewrite <- Qcmult_assoc.
+ rewrite Qcmult_inv_r; auto.
+ apply Qcmult_1_r.
+Qed.
+
+Theorem Qcmult_div_r : forall x y, ~ y = 0 -> y*(x/y) = x.
+Proof.
+ unfold Qcdiv.
+ intros.
+ rewrite Qcmult_assoc.
+ rewrite Qcmult_comm.
+ rewrite Qcmult_assoc.
+ rewrite Qcmult_inv_l; auto.
+ apply Qcmult_1_l.
+Qed.
+
+(** Properties of order upon Q. *)
+
+Lemma Qcle_refl : forall x, x<=x.
+Proof.
+unfold Qcle; intros; simpl; apply Qle_refl.
+Qed.
+
+Lemma Qcle_antisym : forall x y, x<=y -> y<=x -> x=y.
+Proof.
+unfold Qcle; intros; simpl in *.
+apply Qc_is_canon; apply Qle_antisym; auto.
+Qed.
+
+Lemma Qcle_trans : forall x y z, x<=y -> y<=z -> x<=z.
+Proof.
+unfold Qcle; intros; eapply Qle_trans; eauto.
+Qed.
+
+Lemma Qclt_not_eq : forall x y, x<y -> x<>y.
+Proof.
+unfold Qclt; intros; simpl in *.
+intro; destruct (Qlt_not_eq _ _ H).
+subst; auto with qarith.
+Qed.
+
+(** Large = strict or equal *)
+
+Lemma Qclt_le_weak : forall x y, x<y -> x<=y.
+Proof.
+unfold Qcle, Qclt; intros; apply Qlt_le_weak; auto.
+Qed.
+
+Lemma Qcle_lt_trans : forall x y z, x<=y -> y<z -> x<z.
+Proof.
+unfold Qcle, Qclt; intros; eapply Qle_lt_trans; eauto.
+Qed.
+
+Lemma Qclt_le_trans : forall x y z, x<y -> y<=z -> x<z.
+Proof.
+unfold Qcle, Qclt; intros; eapply Qlt_le_trans; eauto.
+Qed.
+
+Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z.
+Proof.
+unfold Qclt; intros; eapply Qlt_trans; eauto.
+Qed.
+
+(** [x<y] iff [~(y<=x)] *)
+
+Lemma Qcnot_lt_le : forall x y, ~ x<y -> y<=x.
+Proof.
+unfold Qcle, Qclt; intros; apply Qnot_lt_le; auto.
+Qed.
+
+Lemma Qcnot_le_lt : forall x y, ~ x<=y -> y<x.
+Proof.
+unfold Qcle, Qclt; intros; apply Qnot_le_lt; auto.
+Qed.
+
+Lemma Qclt_not_le : forall x y, x<y -> ~ y<=x.
+Proof.
+unfold Qcle, Qclt; intros; apply Qlt_not_le; auto.
+Qed.
+
+Lemma Qcle_not_lt : forall x y, x<=y -> ~ y<x.
+Proof.
+unfold Qcle, Qclt; intros; apply Qle_not_lt; auto.
+Qed.
+
+Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y.
+Proof.
+unfold Qcle, Qclt; intros; apply Qle_lt_or_eq; auto.
+Qed.
+
+(** Some decidability results about orders. *)
+
+Lemma Qc_dec : forall x y, {x<y} + {y<x} + {x=y}.
+Proof.
+unfold Qclt, Qcle; intros.
+destruct (Q_dec x y) as [H|H].
+left; auto.
+right; apply Qc_is_canon; auto.
+Defined.
+
+Lemma Qclt_le_dec : forall x y, {x<y} + {y<=x}.
+Proof.
+unfold Qclt, Qcle; intros; apply Qlt_le_dec; auto.
+Defined.
+
+(** Compatibility of operations with respect to order. *)
+
+Lemma Qcopp_le_compat : forall p q, p<=q -> -q <= -p.
+Proof.
+unfold Qcle, Qcopp; intros; simpl in *.
+repeat rewrite Qred_correct.
+apply Qopp_le_compat; auto.
+Qed.
+
+Lemma Qcle_minus_iff : forall p q, p <= q <-> 0 <= q+-p.
+Proof.
+unfold Qcle, Qcminus; intros; simpl in *.
+repeat rewrite Qred_correct.
+apply Qle_minus_iff; auto.
+Qed.
+
+Lemma Qclt_minus_iff : forall p q, p < q <-> 0 < q+-p.
+Proof.
+unfold Qclt, Qcplus, Qcopp; intros; simpl in *.
+repeat rewrite Qred_correct.
+apply Qlt_minus_iff; auto.
+Qed.
+
+Lemma Qcplus_le_compat :
+ forall x y z t, x<=y -> z<=t -> x+z <= y+t.
+Proof.
+unfold Qcplus, Qcle; intros; simpl in *.
+repeat rewrite Qred_correct.
+apply Qplus_le_compat; auto.
+Qed.
+
+Lemma Qcmult_le_compat_r : forall x y z, x <= y -> 0 <= z -> x*z <= y*z.
+Proof.
+unfold Qcmult, Qcle; intros; simpl in *.
+repeat rewrite Qred_correct.
+apply Qmult_le_compat_r; auto.
+Qed.
+
+Lemma Qcmult_lt_0_le_reg_r : forall x y z, 0 <  z  -> x*z <= y*z -> x <= y.
+Proof.
+unfold Qcmult, Qcle, Qclt; intros; simpl in *.
+repeat progress rewrite Qred_correct in * |-. 
+eapply Qmult_lt_0_le_reg_r; eauto.
+Qed.
+
+Lemma Qcmult_lt_compat_r : forall x y z, 0 < z  -> x < y -> x*z < y*z.
+Proof.
+unfold Qcmult, Qclt; intros; simpl in *.
+repeat progress rewrite Qred_correct in *. 
+eapply Qmult_lt_compat_r; eauto.
+Qed.
+
+(** Rational to the n-th power *)
+
+Fixpoint Qcpower (q:Qc)(n:nat) { struct n } : Qc := 
+ match n with 
+  | O => 1
+  | S n => q * (Qcpower q n)
+ end. 
+
+Notation " q ^ n " := (Qcpower q n) : Qc_scope.
+
+Lemma Qcpower_1 : forall n, 1^n = 1.
+Proof.
+induction n; simpl; auto with qarith.
+rewrite IHn; auto with qarith.
+Qed.
+
+Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0.
+Proof.
+destruct n; simpl.
+destruct 1; auto.
+intros. 
+apply Qc_is_canon.
+simpl.
+compute; auto.
+Qed.
+
+Lemma Qpower_pos : forall p n, 0 <= p -> 0 <= p^n.
+Proof.
+induction n; simpl; auto with qarith.
+intros; compute; intro; discriminate.
+intros.
+apply Qcle_trans with (0*(p^n)).
+compute; intro; discriminate.
+apply Qcmult_le_compat_r; auto.
+Qed.
+
+(** And now everything is easier concerning tactics: *)
+
+(** A ring tactic for rational numbers *)
+
+Definition Qc_eq_bool (x y : Qc) :=
+  if Qc_eq_dec x y then true else false.
+
+Lemma Qc_eq_bool_correct : forall x y : Qc, Qc_eq_bool x y = true -> x=y.
+intros x y; unfold Qc_eq_bool in |- *; case (Qc_eq_dec x y); simpl in |- *; auto.
+intros _ H; inversion H.
+Qed.
+
+Definition Qcrt : Ring_Theory Qcplus Qcmult 1 0 Qcopp Qc_eq_bool.
+Proof.
+constructor.
+exact Qcplus_comm.
+exact Qcplus_assoc.
+exact Qcmult_comm.
+exact Qcmult_assoc.
+exact Qcplus_0_l.
+exact Qcmult_1_l.
+exact Qcplus_opp_r.
+exact Qcmult_plus_distr_l.
+unfold Is_true; intros x y; generalize (Qc_eq_bool_correct x y);
+ case (Qc_eq_bool x y); auto.
+Qed.
+
+Add Ring Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcrt [ Qcmake ].
+
+(** A field tactic for rational numbers *)
+
+Require Import Field.
+
+Add Field Qc Qcplus Qcmult 1 0 Qcopp Qc_eq_bool Qcinv Qcrt Qcmult_inv_l
+ with div:=Qcdiv.
+
+Example test_field : forall x y : Qc, y<>0 -> (x/y)*y = x.
+intros.
+field.
+auto.
+Qed.
+
+
+
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 049c195a..c503daad 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qreduction.v 8883 2006-05-31 21:56:37Z letouzey $ i*)
+(*i $Id: Qreduction.v 8989 2006-06-25 22:17:49Z letouzey $ i*)
 
 (** * Normalisation functions for rational numbers. *)
 
@@ -32,65 +32,17 @@ Proof.
  simple destruct z; simpl in |- *; auto; intros; elim H; auto.
 Qed.
 
-(** A simple cancelation by powers of two *)
-
-Fixpoint Pfactor_twos (p p':positive) {struct p} : (positive*positive) := 
- match p, p' with 
-  | xO p, xO p' => Pfactor_twos p p'
-  | _, _ => (p,p')
- end.
-
-Definition Qfactor_twos (q:Q) := 
- let (p,q) := q in 
- match p with 
-   | Z0 => 0
-   | Zpos p => let (p,q) := Pfactor_twos p q in (Zpos p)#q
-   | Zneg p => let (p,q) := Pfactor_twos p q in (Zneg p)#q
- end.
-
-Lemma Pfactor_twos_correct : forall p p', 
-   (p*(snd (Pfactor_twos p p')))%positive = 
-   (p'*(fst (Pfactor_twos p p')))%positive.
-Proof.
-induction p; intros.
-simpl snd; simpl fst; rewrite Pmult_comm; auto.
-destruct p'.
-simpl snd; simpl fst; rewrite Pmult_comm; auto.
-simpl; f_equal; auto.
-simpl snd; simpl fst; rewrite Pmult_comm; auto.
-simpl snd; simpl fst; rewrite Pmult_comm; auto.
-Qed.
-
-Lemma Qfactor_twos_correct : forall q, Qfactor_twos q == q.
-Proof.
-intros (p,q).
-destruct p.
-red; simpl; auto.
-simpl.
-generalize (Pfactor_twos_correct p q); destruct (Pfactor_twos p q).
-red; simpl.
-intros; f_equal.
-rewrite H; apply Pmult_comm.
-simpl.
-generalize (Pfactor_twos_correct p q); destruct (Pfactor_twos p q).
-red; simpl.
-intros; f_equal.
-rewrite H; apply Pmult_comm.
-Qed.
-Hint Resolve Qfactor_twos_correct.
-
 (** Simplification of fractions using [Zgcd].
   This version can compute within Coq. *)
 
 Definition Qred (q:Q) := 
-  let (q1,q2) := Qfactor_twos q in 
-  let (r1,r2) := snd (Zggcd q1 (Zpos q2)) in r1#(Z2P r2).
+  let (q1,q2) := q in 
+  let (r1,r2) := snd (Zggcd q1 ('q2)) 
+  in r1#(Z2P r2).
 
 Lemma Qred_correct : forall q, (Qred q) == q.
 Proof.
-intros; apply Qeq_trans with (Qfactor_twos q); auto.
-unfold Qred.
-destruct (Qfactor_twos q) as (n,d); red; simpl.
+unfold Qred, Qeq; intros (n,d); simpl.
 generalize (Zggcd_gcd n ('d)) (Zgcd_is_pos n ('d)) 
   (Zgcd_is_gcd n ('d)) (Zggcd_correct_divisors n ('d)).
 destruct (Zggcd n (Zpos d)) as (g,(nn,dd)); simpl.
@@ -112,16 +64,8 @@ Qed.
 
 Lemma Qred_complete : forall p q,  p==q -> Qred p = Qred q.
 Proof.
-intros.
-assert (Qfactor_twos p == Qfactor_twos q).
- apply Qeq_trans with p; auto.
- apply Qeq_trans with q; auto.
- symmetry; auto.
-clear H.
-unfold Qred.
-destruct (Qfactor_twos p) as (a,b); 
-destruct (Qfactor_twos q) as (c,d); clear p q.
-unfold Qeq in *; simpl in *.
+intros (a,b) (c,d).
+unfold Qred, Qeq in *; simpl in *.
 Open Scope Z_scope.
 generalize (Zggcd_gcd a ('b)) (Zgcd_is_gcd a ('b)) 
  (Zgcd_is_pos a ('b)) (Zggcd_correct_divisors a ('b)).
@@ -198,47 +142,6 @@ rewrite (Qred_correct q); auto.
 rewrite (Qred_correct q'); auto.
 Qed.
 
-(** Another version, dedicated to extraction *)
-
-Definition Qred_extr (q : Q) :=
-  let (q1, q2) := Qfactor_twos q in
-  let (p,_) := Zggcd_spec_pos (Zpos q2) (Zle_0_pos q2) q1 in  
-  let (r2,r1) := snd p in r1#(Z2P r2).
-
-Lemma Qred_extr_Qred : forall q, Qred_extr q = Qred q.
-Proof.
-unfold Qred, Qred_extr.
-intro q; destruct (Qfactor_twos q) as (n,p); clear q.
-Open Scope Z_scope.
-destruct (Zggcd_spec_pos (' p) (Zle_0_pos p) n) as ((g,(pp,nn)),H).
-generalize (H (Zle_0_pos p)); clear H; intros (Hg1,(Hg2,(Hg4,Hg3))).
-simpl.
-generalize (Zggcd_gcd n ('p)) (Zgcd_is_gcd n ('p)) 
- (Zgcd_is_pos n ('p)) (Zggcd_correct_divisors n ('p)).
-destruct (Zggcd n (Zpos p)) as (g',(nn',pp')); simpl.
-intro H; rewrite <- H; clear H.
-intros Hg'1 Hg'2 (Hg'3,Hg'4).
-assert (g<>0).
- intro; subst g; discriminate.
-destruct (Zis_gcd_uniqueness_apart_sign n ('p) g g'); auto.
-apply Zis_gcd_sym; auto.
-subst g'.
-f_equal.
-apply Zmult_reg_l with g; auto; congruence.
-f_equal.
-apply Zmult_reg_l with g; auto; congruence.
-elimtype False; omega.
-Open Scope Q_scope.
-Qed.
-
-Add Morphism Qred_extr : Qred_extr_comp. 
-Proof.
-intros q q' H.
-do 2 rewrite Qred_extr_Qred.
-rewrite (Qred_correct q); auto.
-rewrite (Qred_correct q'); auto.
-Qed.
-
 Definition Qplus' (p q : Q) := Qred (Qplus p q).
 Definition Qmult' (p q : Q) := Qred (Qmult p q). 
 
diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v
index 6d30e291..0148d0a2 100644
--- a/theories/Reals/Ranalysis1.v
+++ b/theories/Reals/Ranalysis1.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Ranalysis1.v 8670 2006-03-28 22:16:14Z herbelin $ i*)
+(*i $Id: Ranalysis1.v 9042 2006-07-11 22:06:48Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -27,6 +27,18 @@ Definition div_real_fct (a:R) f (x:R) : R := a / f x.
 Definition comp f1 f2 (x:R) : R := f1 (f2 x).
 Definition inv_fct f (x:R) : R := / f x.
 
+Delimit Scope Rfun_scope with F.
+
+Arguments Scope plus_fct [Rfun_scope Rfun_scope R_scope].
+Arguments Scope mult_fct [Rfun_scope Rfun_scope R_scope].
+Arguments Scope minus_fct [Rfun_scope Rfun_scope R_scope].
+Arguments Scope div_fct [Rfun_scope Rfun_scope R_scope].
+Arguments Scope inv_fct [Rfun_scope R_scope].
+Arguments Scope opp_fct [Rfun_scope R_scope].
+Arguments Scope mult_real_fct [R_scope Rfun_scope R_scope].
+Arguments Scope div_real_fct [R_scope Rfun_scope R_scope].
+Arguments Scope comp [Rfun_scope Rfun_scope R_scope].
+
 Infix "+" := plus_fct : Rfun_scope.
 Notation "- x" := (opp_fct x) : Rfun_scope.
 Infix "*" := mult_fct : Rfun_scope.
@@ -36,8 +48,6 @@ Notation Local "f1 'o' f2" := (comp f1 f2)
   (at level 20, right associativity) : Rfun_scope.
 Notation "/ x" := (inv_fct x) : Rfun_scope.
 
-Delimit Scope Rfun_scope with F.
-
 Definition fct_cte (a x:R) : R := a.
 Definition id (x:R) := x.
 
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index b74f7585..e722b679 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -6,21 +6,23 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Znumtheory.v 8853 2006-05-23 18:17:38Z herbelin $ i*)
+(*i $Id: Znumtheory.v 8990 2006-06-26 13:57:44Z notin $ i*)
 
 Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zcomplements.
 Require Import Zdiv.
+Require Import Ndigits.
+Require Import Wf_nat.
 Open Local Scope Z_scope.
 
 (** This file contains some notions of number theory upon Z numbers: 
      - a divisibility predicate [Zdivide]
      - a gcd predicate [gcd]
      - Euclid algorithm [euclid]
-     - an efficient [Zgcd] function 
      - a relatively prime predicate [rel_prime]
      - a prime predicate [prime]
+     - an efficient [Zgcd] function 
 *)
 
 (** * Divisibility *)
@@ -215,6 +217,16 @@ Proof.
 constructor; auto with zarith.
 Qed.
 
+Lemma Zis_gcd_1 : forall a, Zis_gcd a 1 1.
+Proof.
+constructor; auto with zarith.
+Qed.
+
+Lemma Zis_gcd_refl : forall a, Zis_gcd a a a.
+Proof.
+constructor; auto with zarith.
+Qed.
+
 Lemma Zis_gcd_minus : forall a b d:Z, Zis_gcd a (- b) d -> Zis_gcd b a d.
 Proof.
 simple induction 1; constructor; intuition.
@@ -225,6 +237,14 @@ Proof.
 simple induction 1; constructor; intuition.
 Qed.
 
+Lemma Zis_gcd_0_abs : forall a:Z, Zis_gcd 0 a (Zabs a).
+Proof.
+intros a.
+apply Zabs_ind.
+intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto.
+intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto.
+Qed.
+
 Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith.
 
 (** * Extended Euclid algorithm. *)
@@ -366,477 +386,7 @@ replace (c * (u * a + v * b)) with (u * (c * a) + v * (c * b)).
 rewrite H6; rewrite H7; ring.
 ring.
 Qed.
-
-Lemma Zis_gcd_0_abs : forall b, 
- Zis_gcd 0 b (Zabs b) /\ Zabs b >= 0 /\ 0 = Zabs b * 0 /\ b = Zabs b * Zsgn b.
-Proof.
-intro b.
-elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)).
-intros H0; split.
-apply Zabs_ind.
-intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto.
-intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto.
-repeat split; auto with zarith.
-symmetry; apply Zabs_Zsgn.
-
-intros H0; rewrite <- H0.
-rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *.
-split; [ apply Zis_gcd_0 | idtac ]; auto with zarith.
-Qed.
-  
-
-(** We could obtain a [Zgcd] function via [euclid]. But we propose 
-  here a more direct version of a [Zgcd], that can compute within Coq.
-  For that, we use an explicit measure in [nat], and we proved later
-  that using [2(d+1)] is enough, where  [d] is the number of binary digits 
-  of the first argument. *)
-
-Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b => 
- match n with 
-  | O => 1 (* arbitrary, since n should be big enough *)
-  | S n => match a with 
-     | Z0 => Zabs b
-     | Zpos _ => Zgcdn n (Zmod b a) a
-     | Zneg a => Zgcdn n (Zmod b (Zpos a)) (Zpos a)
-     end
-   end.
-
-(* For technical reason, we don't use [Ndigit.Psize] but this 
-   ad-hoc version: [Psize p = S (Psiz p)]. *)
-
-Fixpoint Psiz (p:positive) : nat := 
-  match p with 
-    | xH => O
-    | xI p => S (Psiz p) 
-    | xO p => S (Psiz p)
-  end.
-
-Definition Zgcd_bound (a:Z) := match a with 
- | Z0 => S O
- | Zpos p => let n := Psiz p in S (S (n+n))
- | Zneg p => let n := Psiz p in S (S (n+n))
-end.
-
-Definition Zgcd a b := Zgcdn (Zgcd_bound a) a b.
-
-(** A first obvious fact : [Zgcd a b] is positive. *)
-
-Lemma Zgcdn_is_pos : forall n a b, 
-  0 <= Zgcdn n a b.
-Proof.
-induction n.
-simpl; auto with zarith.
-destruct a; simpl; intros; auto with zarith; auto.
-Qed.
-
-Lemma Zgcd_is_pos : forall a b, 0 <= Zgcd a b.
-Proof.
-intros; unfold Zgcd; apply Zgcdn_is_pos; auto.
-Qed.
-
-(** We now prove that Zgcd is indeed a gcd. *)
-
-(** 1) We prove a weaker & easier bound. *)
-
-Lemma Zgcdn_linear_bound : forall n a b, 
- Zabs a < Z_of_nat n -> Zis_gcd a b (Zgcdn n a b).
-Proof.
-induction n.
-simpl; intros.
-elimtype False; generalize (Zabs_pos a); omega.
-destruct a; intros; simpl; 
- [ generalize (Zis_gcd_0_abs b); intuition | | ]; 
- unfold Zmod; 
- generalize (Z_div_mod b (Zpos p) (refl_equal Gt));
- destruct (Zdiv_eucl b (Zpos p)) as (q,r);
- intros (H0,H1); 
- rewrite inj_S in H; simpl Zabs in H; 
- assert (H2: Zabs r < Z_of_nat n) by (rewrite Zabs_eq; auto with zarith);  
- assert (IH:=IHn r (Zpos p) H2); clear IHn; 
- simpl in IH |- *; 
- rewrite H0.
- apply Zis_gcd_for_euclid2; auto.
- apply Zis_gcd_minus; apply Zis_gcd_sym.
- apply Zis_gcd_for_euclid2; auto.
-Qed.
-
-(** 2) For Euclid's algorithm, the worst-case situation corresponds 
-     to Fibonacci numbers. Let's define them: *)
-
-Fixpoint fibonacci (n:nat) : Z := 
- match n with 
-   | O => 1
-   | S O => 1
-   | S (S n as p) => fibonacci p + fibonacci n 
- end.
-
-Lemma fibonacci_pos : forall n, 0 <= fibonacci n.
-Proof.
-cut (forall N n, (n<N)%nat -> 0<=fibonacci n).
-eauto.
-induction N.
-inversion 1.
-intros.
-destruct n.
-simpl; auto with zarith.
-destruct n.
-simpl; auto with zarith.
-change (0 <= fibonacci (S n) + fibonacci n).
-generalize (IHN n) (IHN (S n)); omega.
-Qed.
-
-Lemma fibonacci_incr : 
- forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m.
-Proof.
-induction 1.
-auto with zarith.
-apply Zle_trans with (fibonacci m); auto.
-clear.
-destruct m.
-simpl; auto with zarith.
-change (fibonacci (S m) <= fibonacci (S m)+fibonacci m).
-generalize (fibonacci_pos m); omega.
-Qed.
-
-(** 3) We prove that fibonacci numbers are indeed worst-case: 
-   for a given number [n], if we reach a conclusion about [gcd(a,b)] in 
-   exactly [n+1] loops, then [fibonacci (n+1)<=a /\ fibonacci(n+2)<=b] *)
-
-Lemma Zgcdn_worst_is_fibonacci : forall n a b, 
- 0 < a < b -> 
- Zis_gcd a b (Zgcdn (S n) a b) -> 
- Zgcdn n a b <> Zgcdn (S n) a b -> 
- fibonacci (S n) <= a /\ 
- fibonacci (S (S n)) <= b.
-Proof.
-induction n.
-simpl; intros.
-destruct a; omega.
-intros.
-destruct a; [simpl in *; omega| | destruct H; discriminate].
-revert H1; revert H0.
-set (m:=S n) in *; (assert (m=S n) by auto); clearbody m.
-pattern m at 2; rewrite H0.
-simpl Zgcdn.
-unfold Zmod; generalize (Z_div_mod b (Zpos p) (refl_equal Gt)).
-destruct (Zdiv_eucl b (Zpos p)) as (q,r).
-intros (H1,H2).
-destruct H2.
-destruct (Zle_lt_or_eq _ _ H2).
-generalize (IHn _ _ (conj H4 H3)).
-intros H5 H6 H7. 
-replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto.
-assert (r = Zpos p * (-q) + b) by (rewrite H1; ring).
-destruct H5; auto.
-pattern r at 1; rewrite H8.
-apply Zis_gcd_sym.
-apply Zis_gcd_for_euclid2; auto.
-apply Zis_gcd_sym; auto.
-split; auto.
-rewrite H1.
-apply Zplus_le_compat; auto.
-apply Zle_trans with (Zpos p * 1); auto.
-ring (Zpos p * 1); auto.
-apply Zmult_le_compat_l.
-destruct q.
-omega.
-assert (0 < Zpos p0) by (compute; auto).
-omega.
-assert (Zpos p * Zneg p0 < 0) by (compute; auto).
-omega. 
-compute; intros; discriminate.
-(* r=0 *)
-subst r.
-simpl; rewrite H0.
-intros.
-simpl in H4.
-simpl in H5.
-destruct n.
-simpl in H5.
-simpl.
-omega.
-simpl in H5.
-elim H5; auto.
-Qed.
-
-(** 3b) We reformulate the previous result in a more positive way. *)
-
-Lemma Zgcdn_ok_before_fibonacci : forall n a b, 
- 0 < a < b -> a < fibonacci (S n) ->
- Zis_gcd a b (Zgcdn n a b).
-Proof.
-destruct a; [ destruct 1; elimtype False; omega | | destruct 1; discriminate].
-cut (forall k n b, 
-         k = (S (nat_of_P p) - n)%nat -> 
-         0 < Zpos p < b -> Zpos p < fibonacci (S n) -> 
-         Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)).
-destruct 2; eauto.
-clear n; induction k. 
-intros.
-assert (nat_of_P p < n)%nat by omega.
-apply Zgcdn_linear_bound. 
-simpl.
-generalize (inj_le _ _ H2).
-rewrite inj_S.
-rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto.
-omega.
-intros.
-generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros.
-assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)).
- apply IHk; auto.
- omega.
- replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto.
- generalize (fibonacci_pos n); omega.
-replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto.
-generalize (H2 H3); clear H2 H3; omega.
-Qed.
-
-(** 4) The proposed bound leads to a fibonacci number that is big enough. *)
-
-Lemma Zgcd_bound_fibonacci : 
-  forall a, 0 < a -> a < fibonacci (Zgcd_bound a).
-Proof.
-destruct a; [omega| | intro H; discriminate].
-intros _.
-induction p.
-simpl Zgcd_bound in *.
-rewrite Zpos_xI.
-rewrite plus_comm; simpl plus.
-set (n:=S (Psiz p+Psiz p)) in *.
-change (2*Zpos p+1 < 
- fibonacci (S n) + fibonacci n + fibonacci (S n)).
-generalize (fibonacci_pos n).
-omega.
-simpl Zgcd_bound in *.
-rewrite Zpos_xO.
-rewrite plus_comm; simpl plus.
-set (n:= S (Psiz p +Psiz p)) in *.
-change (2*Zpos p < 
- fibonacci (S n) + fibonacci n + fibonacci (S n)).
-generalize (fibonacci_pos n).
-omega.
-simpl; auto with zarith.
-Qed.
-
-(* 5) the end: we glue everything together and take care of 
-   situations not corresponding to [0<a<b]. *)
-
-Lemma Zgcd_is_gcd : 
-  forall a b, Zis_gcd a b (Zgcd a b).
-Proof.
-unfold Zgcd; destruct a; intros.
-simpl; generalize (Zis_gcd_0_abs b); intuition.
-(*Zpos*)
-generalize (Zgcd_bound_fibonacci (Zpos p)).
-simpl Zgcd_bound.
-set (n:=S (Psiz p+Psiz p)); (assert (n=S (Psiz p+Psiz p)) by auto); clearbody n.
-simpl Zgcdn.
-unfold Zmod.
-generalize (Z_div_mod b (Zpos p) (refl_equal Gt)).
-destruct (Zdiv_eucl b (Zpos p)) as (q,r).
-intros (H1,H2) H3.
-rewrite H1.
-apply Zis_gcd_for_euclid2.
-destruct H2.
-destruct (Zle_lt_or_eq _ _ H0).
-apply Zgcdn_ok_before_fibonacci; auto; omega.
-subst r n; simpl.
-apply Zis_gcd_sym; apply Zis_gcd_0.
-(*Zneg*)
-generalize (Zgcd_bound_fibonacci (Zpos p)).
-simpl Zgcd_bound.
-set (n:=S (Psiz p+Psiz p)); (assert (n=S (Psiz p+Psiz p)) by auto); clearbody n.
-simpl Zgcdn.
-unfold Zmod.
-generalize (Z_div_mod b (Zpos p) (refl_equal Gt)).
-destruct (Zdiv_eucl b (Zpos p)) as (q,r).
-intros (H1,H2) H3.
-rewrite H1.
-apply Zis_gcd_minus.
-apply Zis_gcd_sym.
-apply Zis_gcd_for_euclid2.
-destruct H2.
-destruct (Zle_lt_or_eq _ _ H0).
-apply Zgcdn_ok_before_fibonacci; auto; omega.
-subst r n; simpl.
-apply Zis_gcd_sym; apply Zis_gcd_0.
-Qed.
-
-(** A generalized gcd: it additionnally keeps track of the divisors. *)
-
-Fixpoint Zggcdn (n:nat) : Z -> Z -> (Z*(Z*Z)) := fun a b => 
- match n with 
-  | O => (1,(a,b))   (*(Zabs b,(0,Zsgn b))*)
-  | S n => match a with 
-     | Z0 => (Zabs b,(0,Zsgn b))
-     | Zpos _ => 
-               let (q,r) := Zdiv_eucl b a in   (* b = q*a+r *)
-               let (g,p) := Zggcdn n r a in 
-               let (rr,aa) := p in        (* r = g *rr /\ a = g * aa *)
-               (g,(aa,q*aa+rr))
-     | Zneg a => 
-               let (q,r) := Zdiv_eucl b (Zpos a) in  (* b = q*(-a)+r *)
-               let (g,p) := Zggcdn n r (Zpos a) in 
-               let (rr,aa) := p in         (* r = g*rr /\ (-a) = g * aa *)  
-               (g,(-aa,q*aa+rr))
-     end
-   end.
-
-Definition Zggcd a b : Z * (Z * Z) := Zggcdn (Zgcd_bound a) a b.
-
-(** The first component of [Zggcd] is [Zgcd] *) 
-
-Lemma Zggcdn_gcdn : forall n a b, 
- fst (Zggcdn n a b) = Zgcdn n a b.
-Proof.
-induction n; simpl; auto.
-destruct a; unfold Zmod; simpl; intros; auto; 
- destruct (Zdiv_eucl b (Zpos p)) as (q,r); 
- rewrite <- IHn; 
- destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)); simpl; auto.
-Qed.
-
-Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b.
-Proof.
-intros; unfold Zggcd, Zgcd; apply Zggcdn_gcdn; auto.
-Qed.
-
-(** [Zggcd] always returns divisors that are coherent with its 
- first output. *)
-
-Lemma Zggcdn_correct_divisors : forall n a b, 
-  let (g,p) := Zggcdn n a b in 
-  let (aa,bb):=p in 
-  a=g*aa /\ b=g*bb.
-Proof.
-induction n.
-simpl.
-split; [destruct a|destruct b]; auto.
-intros.
-simpl.
-destruct a.
-rewrite Zmult_comm; simpl.
-split; auto.
-symmetry; apply Zabs_Zsgn.
-generalize (Z_div_mod b (Zpos p)); 
-destruct (Zdiv_eucl b (Zpos p)) as (q,r).
-generalize (IHn r (Zpos p)); 
-destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)).
-intuition.
-destruct H0.
-compute; auto.
-rewrite H; rewrite H1; rewrite H2; ring.
-generalize (Z_div_mod b (Zpos p)); 
-destruct (Zdiv_eucl b (Zpos p)) as (q,r).
-destruct 1.
-compute; auto.
-generalize (IHn r (Zpos p)); 
-destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)).
-intuition.
-destruct H0.
-replace (Zneg p) with (-Zpos p) by compute; auto.
-rewrite H4; ring.
-rewrite H; rewrite H4; rewrite H0; ring.
-Qed.
-
-Lemma Zggcd_correct_divisors : forall a b, 
-  let (g,p) := Zggcd a b in 
-  let (aa,bb):=p in 
-  a=g*aa /\ b=g*bb.
-Proof.
-unfold Zggcd; intros; apply Zggcdn_correct_divisors; auto.
-Qed.
- 
-(** Due to the use of an explicit measure, the extraction of [Zgcd] 
-  isn't optimal. We propose here another version [Zgcd_spec] that 
-  doesn't suffer from this problem (but doesn't compute in Coq). *)
-
-Definition Zgcd_spec_pos :
-  forall a:Z,
-    0 <= a -> forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}.
-Proof.
-intros a Ha.
-apply
- (Zlt_0_rec
-    (fun a:Z => forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}));
- try assumption.
-intro x; case x.
-intros _ _ b; exists (Zabs b).
-generalize (Zis_gcd_0_abs b); intuition.
   
-intros p Hrec _ b.
-generalize (Z_div_mod b (Zpos p)).
-case (Zdiv_eucl b (Zpos p)); intros q r Hqr.
-elim Hqr; clear Hqr; intros; auto with zarith.
-elim (Hrec r H0 (Zpos p)); intros g Hgkl.
-inversion_clear H0.
-elim (Hgkl H1); clear Hgkl; intros H3 H4.
-exists g; intros.
-split; auto.
-rewrite H.
-apply Zis_gcd_for_euclid2; auto.
-
-intros p _ H b.
-elim H; auto.
-Defined.
-
-Definition Zgcd_spec : forall a b:Z, {g : Z | Zis_gcd a b g /\ g >= 0}.
-Proof.
-intros a; case (Z_gt_le_dec 0 a).
-intros; assert (0 <= - a).
-omega.
-elim (Zgcd_spec_pos (- a) H b); intros g Hgkl.
-exists g.
-intuition.
-intros Ha b; elim (Zgcd_spec_pos a Ha b); intros g; exists g; intuition.
-Defined.
-
-(** A last version aimed at extraction that also returns the divisors. *)
-
-Definition Zggcd_spec_pos :
-  forall a:Z,
-    0 <= a -> forall b:Z, {p : Z*(Z*Z) | let (g,p):=p in let (aa,bb):=p in 
-                                       0 <= a -> Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}.
-Proof.
-intros a Ha.
-pattern a; apply Zlt_0_rec; try assumption.
-intro x; case x.
-intros _ _ b; exists (Zabs b,(0,Zsgn b)).
-intros _; apply Zis_gcd_0_abs.
-  
-intros p Hrec _ b.
-generalize (Z_div_mod b (Zpos p)).
-case (Zdiv_eucl b (Zpos p)); intros q r Hqr.
-elim Hqr; clear Hqr; intros; auto with zarith.
-destruct (Hrec r H0 (Zpos p)) as ((g,(rr,pp)),Hgkl).
-destruct H0.
-destruct (Hgkl H0) as (H3,(H4,(H5,H6))).
-exists (g,(pp,pp*q+rr)); intros.
-split; auto.
-rewrite H.
-apply Zis_gcd_for_euclid2; auto.
-repeat split; auto.
-rewrite H; rewrite H6; rewrite H5; ring.
-
-intros p _ H b.
-elim H; auto.
-Defined.
-
-Definition Zggcd_spec : 
- forall a b:Z, {p : Z*(Z*Z) |  let (g,p):=p in let (aa,bb):=p in 
-                                          Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}.
-Proof.
-intros a; case (Z_gt_le_dec 0 a).
-intros; assert (0 <= - a).
-omega.
-destruct (Zggcd_spec_pos (- a) H b) as ((g,(aa,bb)),Hgkl).
-exists (g,(-aa,bb)).
-intuition.
-rewrite <- Zopp_mult_distr_r.
-rewrite <- H2; auto with zarith.
-intros Ha b; elim (Zggcd_spec_pos a Ha b); intros p; exists p.
- repeat destruct p; intuition.
-Defined.
 
 (** * Relative primality *)
 
@@ -920,32 +470,25 @@ assert (g <> 0).
  elim H4; intros.
  rewrite H2 in H6; subst b; omega.
 unfold rel_prime in |- *.
-elim (Zgcd_spec (a / g) (b / g)); intros g' [H3 H4].
-assert (H5 := Zis_gcd_mult _ _ g _ H3).
-rewrite <- Z_div_exact_2 in H5; auto with zarith.
-rewrite <- Z_div_exact_2 in H5; auto with zarith.
-elim (Zis_gcd_uniqueness_apart_sign _ _ _ _ H1 H5).
-intros; rewrite (Zmult_reg_l 1 g' g); auto with zarith.
-intros; rewrite (Zmult_reg_l 1 (- g') g); auto with zarith.
-pattern g at 1 in |- *; rewrite H6; ring.
-
-elim H1; intros.
-elim H7; intros.
-rewrite H9.
-replace (q * g) with (0 + q * g).
-rewrite Z_mod_plus.
-compute in |- *; auto.
-omega.
-ring.
-
-elim H1; intros.
-elim H6; intros.
-rewrite H9.
-replace (q * g) with (0 + q * g).
-rewrite Z_mod_plus.
-compute in |- *; auto.
-omega.
-ring.
+destruct H1.
+destruct H1 as (a',H1).
+destruct H3 as (b',H3).
+replace (a/g) with a'; 
+ [|rewrite H1; rewrite Z_div_mult; auto with zarith].
+replace (b/g) with b'; 
+ [|rewrite H3; rewrite Z_div_mult; auto with zarith].
+constructor.
+exists a'; auto with zarith.
+exists b'; auto with zarith.
+intros x (xa,H5) (xb,H6).
+destruct (H4 (x*g)).
+exists xa; rewrite Zmult_assoc; rewrite <- H5; auto.
+exists xb; rewrite Zmult_assoc; rewrite <- H6; auto.
+replace g with (1*g) in H7; auto with zarith.
+do 2 rewrite Zmult_assoc in H7.
+generalize (Zmult_reg_r _ _ _ H2 H7); clear H7; intros.
+rewrite Zmult_1_r in H7.
+exists q; auto with zarith.
 Qed.
 
 (** * Primality *)
@@ -1045,3 +588,350 @@ case (Zdivide_dec p a); intuition.
 right; apply Gauss with a; auto with zarith.
 Qed.
 
+
+(** We could obtain a [Zgcd] function via Euclid algorithm. But we propose 
+  here a binary version of [Zgcd], faster and executable within Coq.
+
+   Algorithm: 
+
+   gcd 0 b = b
+   gcd a 0 = a
+   gcd (2a) (2b) = 2(gcd a b)
+   gcd (2a+1) (2b) = gcd (2a+1) b
+   gcd (2a) (2b+1) = gcd a (2b+1)
+   gcd (2a+1) (2b+1) = gcd (b-a) (2*a+1)
+                    or gcd (a-b) (2*b+1), depending on whether a<b 
+*)   
+
+Open Scope positive_scope.
+
+Fixpoint Pgcdn (n: nat) (a b : positive) { struct n } : positive := 
+ match n with 
+  | O => 1
+  | S n => 
+     match a,b with 
+       | xH, _ => 1 
+       | _, xH => 1
+       | xO a, xO b => xO (Pgcdn n a b)
+       | a, xO b => Pgcdn n a b
+       | xO a, b => Pgcdn n a b
+       | xI a', xI b' => match Pcompare a' b' Eq with 
+           | Eq => a
+           | Lt => Pgcdn  n (b'-a') a
+           | Gt => Pgcdn n (a'-b') b
+         end
+     end
+  end.
+
+Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := 
+ match n with 
+  | O => (1,(a,b))
+  | S n => 
+     match a,b with 
+       | xH, b => (1,(1,b)) 
+       | a, xH => (1,(a,1))
+       | xO a, xO b => 
+             let (g,p) := Pggcdn n a b in 
+             (xO g,p)
+       | a, xO b => 
+             let (g,p) := Pggcdn n a b in 
+             let (aa,bb) := p in 
+             (g,(aa, xO bb))
+       | xO a, b => 
+             let (g,p) := Pggcdn n a b in 
+             let (aa,bb) := p in 
+             (g,(xO aa, bb))
+       | xI a', xI b' => match Pcompare a' b' Eq with 
+           | Eq => (a,(1,1))
+           | Lt => 
+                let (g,p) := Pggcdn n (b'-a') a in 
+                let (ba,aa) := p in 
+                (g,(aa, aa + xO ba))
+           | Gt => 
+                let (g,p) := Pggcdn n (a'-b') b in 
+                let (ab,bb) := p in 
+                (g,(bb+xO ab, bb))
+         end
+     end
+  end.
+
+Definition Pgcd (a b: positive) := Pgcdn (Psize a + Psize b)%nat a b.
+Definition Pggcd (a b: positive) := Pggcdn (Psize a + Psize b)%nat a b.
+
+Open Scope Z_scope.
+
+Definition Zgcd (a b : Z) : Z := match a,b with 
+  | Z0, _ => Zabs b 
+  | _, Z0 => Zabs a
+  | Zpos a, Zpos b => Zpos (Pgcd a b)
+  | Zpos a, Zneg b => Zpos (Pgcd a b)
+  | Zneg a, Zpos b => Zpos (Pgcd a b)
+  | Zneg a, Zneg b => Zpos (Pgcd a b)
+end.
+
+Definition Zggcd (a b : Z) : Z*(Z*Z) := match a,b with 
+  | Z0, _ => (Zabs b,(0, Zsgn b)) 
+  | _, Z0 => (Zabs a,(Zsgn a, 0))
+  | Zpos a, Zpos b => 
+     let (g,p) := Pggcd a b in 
+     let (aa,bb) := p in 
+     (Zpos g, (Zpos aa, Zpos bb))
+  | Zpos a, Zneg b => 
+     let (g,p) := Pggcd a b in 
+     let (aa,bb) := p in 
+     (Zpos g, (Zpos aa, Zneg bb))
+  | Zneg a, Zpos b => 
+     let (g,p) := Pggcd a b in 
+     let (aa,bb) := p in 
+     (Zpos g, (Zneg aa, Zpos bb))
+  | Zneg a, Zneg b =>
+     let (g,p) := Pggcd a b in 
+     let (aa,bb) := p in 
+     (Zpos g, (Zneg aa, Zneg bb))
+end.
+
+Lemma Zgcd_is_pos : forall a b, 0 <= Zgcd a b.
+Proof.
+unfold Zgcd; destruct a; destruct b; auto with zarith.
+Qed.
+
+Lemma Psize_monotone : forall p q, Pcompare p q Eq = Lt -> (Psize p <= Psize q)%nat.
+Proof.
+induction p; destruct q; simpl; auto with arith; intros; try discriminate.
+intros; generalize (Pcompare_Gt_Lt _ _ H); auto with arith.
+intros; destruct (Pcompare_Lt_Lt _ _ H); auto with arith; subst; auto.
+Qed.
+
+Lemma Pminus_Zminus : forall a b, Pcompare a b Eq = Lt -> 
+ Zpos (b-a) = Zpos b - Zpos a.
+Proof.
+intros.
+repeat rewrite Zpos_eq_Z_of_nat_o_nat_of_P.
+rewrite nat_of_P_minus_morphism.
+apply inj_minus1.
+apply lt_le_weak.
+apply nat_of_P_lt_Lt_compare_morphism; auto.
+rewrite ZC4; rewrite H; auto.
+Qed.
+
+Lemma Zis_gcd_even_odd : forall a b g, Zis_gcd (Zpos a) (Zpos (xI b)) g -> 
+ Zis_gcd (Zpos (xO a)) (Zpos (xI b)) g. 
+Proof.
+intros.
+destruct H.
+constructor; auto.
+destruct H as (e,H2); exists (2*e); auto with zarith.
+rewrite Zpos_xO; rewrite H2; ring.
+intros.
+apply H1; auto.
+rewrite Zpos_xO in H2.
+rewrite Zpos_xI in H3.
+apply Gauss with 2; auto.
+apply bezout_rel_prime.
+destruct H3 as (bb, H3).
+apply Bezout_intro with bb (-Zpos b).
+omega.
+Qed.
+
+Lemma Pgcdn_correct : forall n a b, (Psize a + Psize b<=n)%nat -> 
+ Zis_gcd (Zpos a) (Zpos b) (Zpos (Pgcdn n a b)).
+Proof.
+intro n; pattern n; apply lt_wf_ind; clear n; intros.
+destruct n.
+simpl.
+destruct a; simpl in *; try inversion H0.
+destruct a.
+destruct b; simpl.
+case_eq (Pcompare a b Eq); intros.
+(* a = xI, b = xI, compare = Eq *)
+rewrite (Pcompare_Eq_eq _ _ H1); apply Zis_gcd_refl.
+(* a = xI, b = xI, compare = Lt *)
+apply Zis_gcd_sym.
+apply Zis_gcd_for_euclid with 1.
+apply Zis_gcd_sym.
+replace (Zpos (xI b) - 1 * Zpos (xI a)) with (Zpos(xO (b - a))).
+apply Zis_gcd_even_odd.
+apply H; auto.
+simpl in *.
+assert (Psize (b-a) <= Psize b)%nat.
+ apply Psize_monotone.
+ change (Zpos (b-a) < Zpos b).
+ rewrite (Pminus_Zminus _ _ H1).
+ assert (0 < Zpos a) by (compute; auto).
+ omega.
+omega.  
+rewrite Zpos_xO; do 2 rewrite Zpos_xI.
+rewrite Pminus_Zminus; auto.
+omega.
+(* a = xI, b = xI, compare = Gt *)
+apply Zis_gcd_for_euclid with 1.
+replace (Zpos (xI a) - 1 * Zpos (xI b)) with (Zpos(xO (a - b))).
+apply Zis_gcd_sym.
+apply Zis_gcd_even_odd.
+apply H; auto.
+simpl in *.
+assert (Psize (a-b) <= Psize a)%nat.
+ apply Psize_monotone.
+ change (Zpos (a-b) < Zpos a).
+ rewrite (Pminus_Zminus b a).
+ assert (0 < Zpos b) by (compute; auto).
+ omega.
+ rewrite ZC4; rewrite H1; auto.
+omega.  
+rewrite Zpos_xO; do 2 rewrite Zpos_xI.
+rewrite Pminus_Zminus; auto.
+omega.
+rewrite ZC4; rewrite H1; auto.
+(* a = xI, b = xO *)
+apply Zis_gcd_sym.
+apply Zis_gcd_even_odd.
+apply Zis_gcd_sym.
+apply H; auto.
+simpl in *; omega.
+(* a = xI, b = xH *)
+apply Zis_gcd_1.
+destruct b; simpl.
+(* a = xO, b = xI *)
+apply Zis_gcd_even_odd.
+apply H; auto.
+simpl in *; omega.
+(* a = xO, b = xO *)
+rewrite (Zpos_xO a); rewrite (Zpos_xO b); rewrite (Zpos_xO (Pgcdn n a b)).
+apply Zis_gcd_mult.
+apply H; auto.
+simpl in *; omega.
+(* a = xO, b = xH *)
+apply Zis_gcd_1.
+(* a = xH *)
+simpl; apply Zis_gcd_sym; apply Zis_gcd_1.
+Qed.
+
+Lemma Pgcd_correct : forall a b, Zis_gcd (Zpos a) (Zpos b) (Zpos (Pgcd a b)).
+Proof.
+unfold Pgcd; intros.
+apply Pgcdn_correct; auto.
+Qed.
+
+Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Zgcd a b).
+Proof.
+destruct a.
+intros.
+simpl.
+apply Zis_gcd_0_abs.
+destruct b; simpl.
+apply Zis_gcd_0.
+apply Pgcd_correct.
+apply Zis_gcd_sym.
+apply Zis_gcd_minus; simpl.
+apply Pgcd_correct.
+destruct b; simpl.
+apply Zis_gcd_minus; simpl.
+apply Zis_gcd_sym.
+apply Zis_gcd_0.
+apply Zis_gcd_minus; simpl.
+apply Zis_gcd_sym.
+apply Pgcd_correct.
+apply Zis_gcd_sym.
+apply Zis_gcd_minus; simpl.
+apply Zis_gcd_minus; simpl.
+apply Zis_gcd_sym.
+apply Pgcd_correct.
+Qed.
+
+
+Lemma Pggcdn_gcdn : forall n a b, 
+ fst (Pggcdn n a b) = Pgcdn n a b.
+Proof.
+induction n.
+simpl; auto.
+destruct a; destruct b; simpl; auto.
+destruct (Pcompare a b Eq); simpl; auto.
+rewrite <- IHn; destruct (Pggcdn n (b-a) (xI a)) as (g,(aa,bb)); simpl; auto.
+rewrite <- IHn; destruct (Pggcdn n (a-b) (xI b)) as (g,(aa,bb)); simpl; auto.
+rewrite <- IHn; destruct (Pggcdn n (xI a) b) as (g,(aa,bb)); simpl; auto.
+rewrite <- IHn; destruct (Pggcdn n a (xI b)) as (g,(aa,bb)); simpl; auto.
+rewrite <- IHn; destruct (Pggcdn n a b) as (g,(aa,bb)); simpl; auto.
+Qed.
+
+Lemma Pggcd_gcd : forall a b, fst (Pggcd a b) = Pgcd a b.
+Proof.
+intros; exact (Pggcdn_gcdn (Psize a+Psize b)%nat a b).
+Qed.
+
+Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b.
+Proof.
+destruct a; destruct b; simpl; auto; rewrite <- Pggcd_gcd; 
+destruct (Pggcd p p0) as (g,(aa,bb)); simpl; auto.
+Qed.
+
+Open Scope positive_scope.
+
+Lemma Pggcdn_correct_divisors : forall n a b, 
+  let (g,p) := Pggcdn n a b in 
+  let (aa,bb):=p in 
+  (a=g*aa) /\ (b=g*bb).
+Proof.
+induction n.
+simpl; auto.
+destruct a; destruct b; simpl; auto.
+case_eq (Pcompare a b Eq); intros.
+(* Eq *)
+rewrite Pmult_comm; simpl; auto.
+rewrite (Pcompare_Eq_eq _ _ H); auto.
+(* Lt *)
+generalize (IHn (b-a) (xI a)); destruct (Pggcdn n (b-a) (xI a)) as (g,(ba,aa)); simpl.
+intros (H0,H1); split; auto.
+rewrite Pmult_plus_distr_l.
+rewrite Pmult_xO_permute_r.
+rewrite <- H1; rewrite <- H0.
+simpl; f_equal; symmetry.
+apply Pplus_minus; auto.
+rewrite ZC4; rewrite H; auto.
+(* Gt *)
+generalize (IHn (a-b) (xI b)); destruct (Pggcdn n (a-b) (xI b)) as (g,(ab,bb)); simpl.
+intros (H0,H1); split; auto.
+rewrite Pmult_plus_distr_l.
+rewrite Pmult_xO_permute_r.
+rewrite <- H1; rewrite <- H0.
+simpl; f_equal; symmetry.
+apply Pplus_minus; auto.
+(* Then... *) 
+generalize (IHn (xI a) b); destruct (Pggcdn n (xI a) b) as (g,(ab,bb)); simpl.
+intros (H0,H1); split; auto.
+rewrite Pmult_xO_permute_r; rewrite H1; auto.
+generalize (IHn a (xI b)); destruct (Pggcdn n a (xI b)) as (g,(ab,bb)); simpl.
+intros (H0,H1); split; auto.
+rewrite Pmult_xO_permute_r; rewrite H0; auto.
+generalize (IHn a b); destruct (Pggcdn n a b) as (g,(ab,bb)); simpl.
+intros (H0,H1); split; subst; auto.
+Qed.
+
+Lemma Pggcd_correct_divisors : forall a b, 
+  let (g,p) := Pggcd a b in 
+  let (aa,bb):=p in 
+  (a=g*aa) /\ (b=g*bb).
+Proof.
+intros a b; exact (Pggcdn_correct_divisors (Psize a + Psize b)%nat a b).
+Qed.
+
+Open Scope Z_scope.
+
+Lemma Zggcd_correct_divisors : forall a b, 
+  let (g,p) := Zggcd a b in 
+  let (aa,bb):=p in 
+  (a=g*aa) /\ (b=g*bb).
+Proof.
+destruct a; destruct b; simpl; auto; try solve [rewrite Pmult_comm; simpl; auto]; 
+generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb)); 
+destruct 1; subst; auto.
+Qed.
+
+Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}.
+Proof.
+  intros x y; exists (Zgcd x y).
+  split; [apply Zgcd_is_gcd  | apply Zgcd_is_pos].
+Qed.
+
+
+
+