Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

33 files changed, 370 insertions, 202 deletions

diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index a3b4e647..e46f1279 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ListTactics.v 9290 2006-10-26 19:20:42Z herbelin $ i*)
+(*i $Id: ListTactics.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import BinPos.
 Require Import List.
@@ -17,6 +17,14 @@ Ltac list_fold_right fcons fnil l :=
   | nil => fnil
   end.
 
+Ltac lazy_list_fold_right fcons fnil l :=
+  match l with
+  | (cons ?x ?tl) => 
+       let cont := lazy_list_fold_right fcons fnil in
+       fcons x cont tl
+  | nil => fnil 
+  end.
+
 Ltac list_fold_left fcons fnil l :=
   match l with
   | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 7053266a..1f1c34bf 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalDescription.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
+(*i $Id: ClassicalDescription.v 9514 2007-01-22 14:58:50Z herbelin $ i*)
 
 (** This file provides classical logic and definite description *)
 
@@ -57,14 +57,11 @@ Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) :
   (exists! x:A, P x) -> P (iota i P)
   := proj2_sig (classical_definite_description P i).
 
-(** Weaker lemmas (compatibility lemmas) *)
-
-Unset Implicit Arguments.
-
-Lemma dependent_description :
-    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
-      (forall x:A, exists! y : B x, R x y) ->
-      (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+(** Axiom of unique "choice" (functional reification of functional relations) *)
+Theorem dependent_unique_choice :
+  forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
+    (forall x:A, exists! y : B x, R x y) ->
+    (exists f : (forall x:A, B x), forall x:A, R x (f x)).
 Proof.
 intros A B R H.
 assert (Hexuni:forall x, exists! y, R x y).
@@ -74,27 +71,18 @@ intro x.
 apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))).
 Qed.
 
-Theorem description :
- forall (A B:Type) (R:A -> B -> Prop),
-   (forall x : A,  exists! y : B, R x y) ->
-   (exists f : A->B, forall x:A, R x (f x)).
+Theorem unique_choice :
+  forall (A B:Type) (R:A -> B -> Prop),
+    (forall x:A,  exists! y : B, R x y) ->
+    (exists f : A -> B, forall x:A, R x (f x)).
 Proof.
 intros A B.
-apply (dependent_description A (fun _ => B)).
+apply dependent_unique_choice with (B:=fun _:A => B).
 Qed.
 
-(** Axiom of unique "choice" (functional reification of functional relations) *)
+(** Compatibility lemmas *)
 
-Set Implicit Arguments.
-
-Require Import Setoid.
+Unset Implicit Arguments.
 
-Theorem unique_choice :
- forall (A B:Type) (R:A -> B -> Prop),
-   (forall x:A,  exists! y : B, R x y) ->
-   (exists f : A -> B, forall x:A, R x (f x)).
-Proof.
-intros A B R H.
-apply (description A B).
-intro x. apply H.
-Qed.
+Definition dependent_description := dependent_unique_choice.
+Definition description := unique_choice.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
new file mode 100644
index 00000000..61e377ea
--- /dev/null
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -0,0 +1,155 @@
+(************************************************************************)
+(*  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:$ i*)
+
+(** This module proves the constructive description schema, which
+infers the sigma-existence (i.e., [Set]-existence) of a witness to a
+predicate from the regular existence (i.e., [Prop]-existence). One
+requires that the underlying set is countable and that the predicate
+is decidable. *)
+
+(** Coq does not allow case analysis on sort [Set] when the goal is in
+[Prop]. Therefore, one cannot eliminate [exists n, P n] in order to
+show [{n : nat | P n}]. However, one can perform a recursion on an
+inductive predicate in sort [Prop] so that the returning type of the
+recursion is in [Set]. This trick is described in Coq'Art book, Sect.
+14.2.3 and 15.4. In particular, this trick is used in the proof of
+[Acc_iter] in the module Coq.Init.Wf. There, recursion is done on an
+inductive predicate [Acc] and the resulting type is in [Type].
+
+The predicate [Acc] delineates elements that are accessible via a
+given relation [R]. An element is accessible if there are no infinite
+[R]-descending chains starting from it.
+
+To use [Acc_iter], we define a relation R and prove that if [exists n,
+P n] then 0 is accessible with respect to R. Then, by induction on the
+definition of [Acc R 0], we show [{n : nat | P n}]. *)
+
+(** Contributed by Yevgeniy Makarov *)
+
+Require Import Arith.
+
+Section ConstructiveIndefiniteDescription.
+
+Variable P : nat -> Prop.
+
+Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}.
+
+(** To find a witness of [P] constructively, we define an algorithm
+that tries P on all natural numbers starting from 0 and going up. The
+relation [R] describes the connection between the two successive
+numbers we try. Namely, [y] is [R]-less then [x] if we try [y] after
+[x], i.e., [y = S x] and [P x] is false. Then the absence of an
+infinite [R]-descending chain from 0 is equivalent to the termination
+of our searching algorithm. *)
+
+Let R (x y : nat) := (x = S y /\ ~ P y).
+Notation Local "'acc' x" := (Acc R x) (at level 10).
+
+Lemma P_implies_acc : forall x : nat, P x -> acc x.
+Proof.
+intros x H. constructor.
+intros y [_ not_Px]. absurd (P x); assumption.
+Qed.
+
+Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x.
+Proof.
+intros x n; generalize x; clear x; induction n as [|n IH]; simpl.
+apply P_implies_acc.
+intros x H. constructor. intros y [fxy _].
+apply IH. rewrite fxy.
+replace (n + S x) with (S (n + x)); auto with arith.
+Defined.
+
+Corollary P_eventually_implies_acc_ex : (exists n : nat, P n) -> acc 0.
+Proof.
+intros H; elim H. intros x Px. apply P_eventually_implies_acc with (n := x).
+replace (x + 0) with x; auto with arith.
+Defined.
+
+(** In the following statement, we use the trick with recursion on
+[Acc]. This is also where decidability of [P] is used. *)
+
+Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}.
+Proof.
+intros Acc_0. pattern 0. apply Acc_iter with (R := R); [| assumption].
+clear Acc_0; intros x IH.
+destruct (P_decidable x) as [Px | not_Px].
+exists x; simpl; assumption.
+set (y := S x).
+assert (Ryx : R y x). unfold R; split; auto.
+destruct (IH y Ryx) as [n Hn].
+exists n; assumption.
+Defined.
+
+Theorem constructive_indefinite_description_nat : (exists n : nat, P n) -> {n : nat | P n}.
+Proof.
+intros H; apply acc_implies_P_eventually.
+apply P_eventually_implies_acc_ex; assumption.
+Defined.
+
+End ConstructiveIndefiniteDescription.
+
+Section ConstructiveEpsilon.
+
+(** For the current purpose, we say that a set [A] is countable if
+there are functions [f : A -> nat] and [g : nat -> A] such that [g] is
+a left inverse of [f]. *)
+
+Variable A : Type.
+Variable f : A -> nat.
+Variable g : nat -> A.
+
+Hypothesis gof_eq_id : forall x : A, g (f x) = x.
+
+Variable P : A -> Prop.
+
+Hypothesis P_decidable : forall x : A, {P x} + {~ P x}.
+
+Definition P' (x : nat) : Prop := P (g x).
+
+Lemma P'_decidable : forall n : nat, {P' n} + {~ P' n}.
+Proof.
+intro n; unfold P'; destruct (P_decidable (g n)); auto.
+Defined.
+
+Lemma constructive_indefinite_description : (exists x : A, P x) -> {x : A | P x}.
+Proof.
+intro H. assert (H1 : exists n : nat, P' n).
+destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption.
+apply (constructive_indefinite_description_nat P' P'_decidable)  in H1.
+destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption.
+Defined.
+
+Lemma constructive_definite_description : (exists! x : A, P x) -> {x : A | P x}.
+Proof.
+  intros; apply constructive_indefinite_description; firstorder.
+Defined.
+
+Definition epsilon (E : exists x : A, P x) : A
+  := proj1_sig (constructive_indefinite_description E).
+
+Definition epsilon_spec (E : (exists x, P x)) : P (epsilon E)
+  := proj2_sig (constructive_indefinite_description E).
+
+End ConstructiveEpsilon.
+
+Theorem choice :
+  forall (A B : Type) (f : B -> nat) (g : nat -> B),
+    (forall x : B, g (f x) = x) ->
+    forall (R : A -> B -> Prop),
+    (forall (x : A) (y : B), {R x y} + {~ R x y}) ->
+    (forall x : A, exists y : B, R x y) ->
+    (exists f : A -> B, forall x : A, R x (f x)).
+Proof.
+intros A B f g gof_eq_id R R_dec H.
+exists (fun x : A => epsilon B f g gof_eq_id (R x) (R_dec x) (H x)).
+intro x.
+apply (epsilon_spec B f g gof_eq_id (R x) (R_dec x) (H x)).
+Qed.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index a257ef55..94a577ca 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: EqdepFacts.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: EqdepFacts.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
 
 (** This file defines dependent equality and shows its equivalence with
     equality on dependent pairs (inhabiting sigma-types). It derives
@@ -105,8 +105,8 @@ Implicit Arguments eq_dep1 [U P].
 (** Dependent equality is equivalent to equality on dependent pairs *)
 
 Lemma eq_sigS_eq_dep :
-  forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q),
-    existS P p x = existS P q y -> eq_dep p x q y.
+  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
+    existT P p x = existT P q y -> eq_dep p x q y.
 Proof.
   intros.
   dependent rewrite H.
@@ -114,7 +114,7 @@ Proof.
 Qed.
 
 Lemma equiv_eqex_eqdep :
-  forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q),
+  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
    existS P p x = existS P q y <-> eq_dep p x q y.
 Proof.
   split. 
@@ -248,28 +248,13 @@ End Equivalences.
 Section Corollaries.
   
   Variable U:Type.
-  Variable V:Set.
   
   (** UIP implies the injectivity of equality on dependent pairs in Type *)
-
-  Definition Inj_dep_pairT :=
-    forall (P:U -> Type) (p:U) (x y:P p),
-      existT P p x = existT P p y -> x = y.
-  
-  Lemma eq_dep_eq__inj_pairT2 : Eq_dep_eq U -> Inj_dep_pairT.
-  Proof.
-    intro eq_dep_eq; red; intros.
-    apply eq_dep_eq.
-    apply eq_sigT_eq_dep.
-    assumption.
- Qed.
- 
-  (** UIP implies the injectivity of equality on dependent pairs in Set *)
  
- Definition Inj_dep_pairS :=
-   forall (P:V -> Set) (p:V) (x y:P p), existS P p x = existS P p y -> x = y.
+ Definition Inj_dep_pair :=
+   forall (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y.
  
- Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS.
+ Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair.
  Proof.
    intro eq_dep_eq; red; intros.
    apply eq_dep_eq.
@@ -279,6 +264,11 @@ Section Corollaries.
 
 End Corollaries.
 
+Notation Inj_dep_pairS := Inj_dep_pair.
+Notation Inj_dep_pairT := Inj_dep_pair.
+Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2.
+ 
+
 (************************************************************************)
 (** *** C. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *)
 
@@ -303,7 +293,7 @@ Lemma eq_rect_eq :
 Proof M.eq_rect_eq U.
 
 Lemma eq_rec_eq :
-  forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+  forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h.
 Proof (fun p Q => M.eq_rect_eq U p Q).
 
 (** Injectivity of Dependent Equality *)
@@ -333,18 +323,13 @@ End Axioms.
 
 (** UIP implies the injectivity of equality on dependent pairs in Type *)
 
-Lemma inj_pairT2 :
+Lemma inj_pair2 :
  forall (U:Type) (P:U -> Type) (p:U) (x y:P p),
    existT P p x = existT P p y -> x = y.
-Proof (fun U => eq_dep_eq__inj_pairT2 U (eq_dep_eq U)).
-
-(** UIP implies the injectivity of equality on dependent pairs in Set *)
-
-Lemma inj_pair2 :
- forall (U:Set) (P:U -> Set) (p:U) (x y:P p),
-   existS P p x = existS P p y -> x = y.
 Proof (fun U => eq_dep_eq__inj_pair2 U (eq_dep_eq U)).
 
+Notation inj_pairT2 := inj_pair2.
+
 End EqdepTheory.
 
 Implicit Arguments eq_dep [].
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 740fcfcf..103efd22 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Eqdep_dec.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Eqdep_dec.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
 
 (** We prove that there is only one proof of [x=x], i.e [refl_equal x].
     This holds if the equality upon the set of [x] is decidable.
@@ -235,7 +235,7 @@ End DecidableEqDep.
 
 Module Type DecidableSet.
 
-  Parameter U:Set.
+  Parameter U:Type.
   Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
 
 End DecidableSet.
@@ -276,14 +276,6 @@ Module DecidableEqDepSet (M:DecidableSet).
     forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
   Proof N.Streicher_K.
 
-  (** Injectivity of equality on dependent pairs with second component
-      in [Type] *)
-
-  Lemma inj_pairT2 :
-    forall (P:U -> Type) (p:U) (x y:P p),
-      existT P p x = existT P p y -> x = y.
-  Proof N.inj_pairT2.
-
   (** Proof-irrelevance on subsets of decidable sets *)
 
   Lemma inj_pairP2 :
@@ -291,11 +283,16 @@ Module DecidableEqDepSet (M:DecidableSet).
       ex_intro P x p = ex_intro P x q -> p = q.
   Proof N.inj_pairP2.
 
-  (** Injectivity of equality on dependent pairs in [Set] *)
+  (** Injectivity of equality on dependent pairs in [Type] *)
 
   Lemma inj_pair2 :
-    forall (P:U -> Set) (p:U) (x y:P p),
+    forall (P:U -> Type) (p:U) (x y:P p),
       existS P p x = existS P p y -> x = y.
   Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq.
 
+  (** Injectivity of equality on dependent pairs with second component
+      in [Type] *)
+
+  Notation inj_pairT2 := inj_pair2.
+
 End DecidableEqDepSet.
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 6ba6ca3d..94f50bd0 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Nnat.v 8733 2006-04-25 22:52:18Z letouzey $ i*)
+(*i $Id: Nnat.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
-Require Import Arith.
+Require Import Arith_base.
 Require Import Compare_dec.
 Require Import Sumbool.
 Require Import Div2.
@@ -174,4 +174,4 @@ Proof.
   pattern n at 1; rewrite <- (nat_of_N_of_nat n).
   pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
   symmetry; apply nat_of_Ncompare.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 9d294805..f9aa3e50 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qring.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Qring.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Export Ring.
 Require Export QArith_base.
@@ -37,15 +37,15 @@ Proof.
 Qed.
 
 Ltac isQcst t :=
-  let t := eval hnf in t in
-    match t with
-      Qmake ?n ?d =>
-      match isZcst n with
-        true => isZcst d
-	| _ => false
-      end
-      | _ => false
-    end.
+  match t with
+  | inject_Z ?z => isZcst z
+  | Qmake ?n ?d =>
+    match isZcst n with
+      true => isPcst d
+    | _ => false
+    end
+  | _ => false
+  end.
 
 Ltac Qcst t :=
   match isQcst t with
@@ -74,7 +74,7 @@ Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z).
 Qed.
 
 Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2).
-  ring.
+ ring.
 Qed.
 
 Let ex5 : 1+1 == 2#1.
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index fa44b6ff..581c181f 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -6,7 +6,7 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id: AltSeries.v 9245 2006-10-17 12:53:34Z notin $ i*)
+  (*i $Id: AltSeries.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -92,9 +92,9 @@ Proof.
     replace (Un (S (2 * S N)) + (-1 * Un (S (2 * S N)) + Un (S (S (2 * S N)))))
       with (Un (S (S (2 * S N)))); [ idtac | ring ].
   apply H.
-  ring_nat.
+  ring.
   apply HrecN.
-  ring_nat.
+  ring.
 Qed.
 
 (** A more general inequality *)
@@ -300,7 +300,7 @@ Proof.
   do 2 rewrite Rmult_1_r; apply le_INR.
   replace (2 * S n + 1)%nat with (S (S (2 * n + 1))).
   apply le_trans with (S (2 * n + 1)); apply le_n_Sn.
-  ring_nat.
+  ring.
   apply not_O_INR; discriminate.
   apply not_O_INR; replace (2 * n + 1)%nat with (S (2 * n));
     [ discriminate | ring ].
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 48876be2..7dbbd605 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -6,7 +6,7 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id: ArithProp.v 9245 2006-10-17 12:53:34Z notin $ i*)
+  (*i $Id: ArithProp.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rbasic_fun.
@@ -75,7 +75,7 @@ Proof.
   apply H3; assumption.
   right.
   apply H4; assumption.
-  unfold double in |- *; ring.
+  unfold double in |- *;ring.
 Qed.
 
   (* 2m <= 2n => m<=n *)
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index 3719d551..10965951 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -6,7 +6,7 @@
   (*         *       GNU Lesser General Public License Version 2.1        *)
   (************************************************************************)
 
-  (*i $Id: Cos_plus.v 9245 2006-10-17 12:53:34Z notin $ i*)
+  (*i $Id: Cos_plus.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -486,7 +486,7 @@ Proof.
   apply le_trans with (pred N).
   assumption.
   apply le_pred_n.
-  ring_nat.
+  ring.
   apply Rle_trans with
     (sum_f_R0
       (fun k:nat =>
@@ -515,7 +515,7 @@ Proof.
   apply le_trans with (2 * S (S (n0 + n)))%nat.
   replace (2 * S (S (n0 + n)))%nat with (S (2 * S (n0 + n) + 1)).
   apply le_n_Sn.
-  ring_nat.
+  ring.
   omega.
   right.
   unfold Rdiv in |- *; rewrite Rmult_comm.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index ac8ffbeb..d410e14a 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
  
-(*i $Id: Cos_rel.v 9178 2006-09-26 11:18:22Z barras $ i*)
+(*i $Id: Cos_rel.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -109,9 +109,10 @@ pose
              C (2 * S p) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (p - l))) p
     end).
 ring_simplify.
+unfold Rminus.
 replace
 (* (-   old ring compat *)
- (-1 *
+ (-
   sum_f_R0
     (fun k:nat =>
        sum_f_R0
@@ -140,7 +141,6 @@ replace
     (fun l:nat =>
        C (2 * S i) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (i - l))) i) with
  (sum_f_R0 (fun l:nat => Wn (S (2 * l))) i).
-(*rewrite Rplus_comm.*) (* compatibility old ring... *)
 apply sum_decomposition.
 apply sum_eq; intros.
 unfold Wn in |- *.
@@ -154,8 +154,7 @@ apply Rmult_eq_compat_l.
 replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat.
 reflexivity.
 omega.
-replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))).
-(*replace (* compatibility old ring... *)
+replace
  (-
   sum_f_R0
     (fun k:nat =>
@@ -171,13 +170,13 @@ replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))).
          (fun p:nat =>
             (-1) ^ p / INR (fact (2 * p + 1)) * x ^ (2 * p + 1) *
             ((-1) ^ (k - p) / INR (fact (2 * (k - p) + 1)) *
-             y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].*)
-apply Rmult_eq_compat_l.
+             y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].
 rewrite scal_sum.
 rewrite decomp_sum.
 replace (sin_nnn 0%nat) with 0.
-rewrite Rmult_0_l; rewrite Rplus_0_l.
-replace (pred (S n)) with n; [ idtac | reflexivity ].
+rewrite Rplus_0_l.
+change (pred (S n)) with n.
+   (* replace (pred (S n)) with n; [ idtac | reflexivity ]. *)
 apply sum_eq; intros.
 rewrite Rmult_comm.
 unfold sin_nnn in |- *.
@@ -185,8 +184,8 @@ rewrite scal_sum.
 rewrite scal_sum.
 apply sum_eq; intros.
 unfold Rdiv in |- *.
-repeat rewrite Rmult_assoc.
-rewrite (Rmult_comm (/ INR (fact (2 * S i)))).
+(*repeat rewrite Rmult_assoc.*)
+(* rewrite (Rmult_comm (/ INR (fact (2 * S i)))). *)
 repeat rewrite <- Rmult_assoc.
 rewrite <- (Rmult_comm (/ INR (fact (2 * S i)))).
 repeat rewrite <- Rmult_assoc.
@@ -216,7 +215,7 @@ apply INR_fact_neq_0.
 apply INR_fact_neq_0.
 reflexivity.
 apply lt_O_Sn.
-ring.
+(* ring. *)
 apply sum_eq; intros.
 rewrite scal_sum.
 apply sum_eq; intros.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 5dafec83..beb4b744 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Exp_prop.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Exp_prop.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -87,7 +87,7 @@ Proof.
   reflexivity.
   replace (2 * S N)%nat with (S (S (2 * N))).
   simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma div2_S_double : forall N:nat, div2 (S (2 * N)) = N.
@@ -96,7 +96,7 @@ Proof.
   reflexivity.
   replace (2 * S N)%nat with (S (S (2 * N))).
   simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < div2 N)%nat.
@@ -367,7 +367,7 @@ Proof.
   apply le_trans with (pred N).
   apply H0.
   apply le_pred_n.
-  rewrite H4; ring_nat.
+  rewrite H4; ring.
   cut (S N = (2 * S N0)%nat).
   intro.
   replace (C (S N) (S N0) / INR (fact (S N))) with (/ Rsqr (INR (fact (S N0)))).
@@ -388,7 +388,7 @@ Proof.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  rewrite H4; ring_nat.
+  rewrite H4; ring.
   unfold C, Rdiv in |- *.
   rewrite (Rmult_comm (INR (fact (S N)))).
   rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
@@ -494,7 +494,7 @@ Proof.
   simpl in |- *.
   pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
     apply Rlt_0_1.
-  ring_nat.
+  ring.
   unfold Rsqr in |- *; apply prod_neq_R0; apply INR_fact_neq_0.
   unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; discriminate.
   assert (H0 := even_odd_cor N).
@@ -515,7 +515,7 @@ Proof.
   replace (S (S (2 * N0))) with (2 * S N0)%nat.
   do 2 rewrite div2_double.
   reflexivity.
-  ring_nat.
+  ring.
   apply S_pred with 0%nat; apply H.
 Qed.
 
@@ -585,8 +585,8 @@ Proof.
   apply (fun m n p:nat => mult_le_compat_l p n m).
   replace (2 * S N1)%nat with (S (S (2 * N1))).
   apply le_n_Sn.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   reflexivity.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
@@ -623,7 +623,7 @@ Proof.
   replace (2 * N1)%nat with (S (S (2 * pred N1))).
   reflexivity.
   pattern N1 at 2 in |- *; replace N1 with (S (pred N1)).
-  ring_nat.
+  ring.
   symmetry  in |- *; apply S_pred with 0%nat; apply H8.
   apply INR_lt.
   apply Rmult_lt_reg_l with (INR 2).
@@ -641,7 +641,7 @@ Proof.
   rewrite div2_double.
   replace (2 * S N1)%nat with (S (S (2 * N1))).
   apply le_n_Sn.
-  ring_nat.
+  ring.
   reflexivity.
   apply le_trans with (max (2 * S N0) 2).
   apply le_max_l.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 11c6378e..a8f72302 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: PartSum.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: PartSum.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -278,7 +278,7 @@ Proof.
   rewrite (tech5 An (2 * S N)).
   rewrite <- HrecN.
   ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma sum_Rle :
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 51c66afa..7d98a844 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -6,13 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RIneq.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: RIneq.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 (***************************************************************************)
 (**              Basic lemmas for the classical reals numbers              *)
 (***************************************************************************)
 
 Require Export Raxioms.
+Require Import Rpow_def.
+Require Import Zpower.
 Require Export ZArithRing.
 Require Import Omega.
 Require Export RealField.
@@ -1528,6 +1530,16 @@ Proof.
   rewrite Rmult_opp_opp; auto with real.
 Qed.
 
+Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Zpower z (Z_of_nat n)).
+Proof.
+ intros z [|n];simpl;trivial.
+ rewrite Zpower_pos_nat.
+ rewrite nat_of_P_o_P_of_succ_nat_eq_succ. unfold Zpower_nat;simpl.
+ rewrite mult_IZR.
+ induction n;simpl;trivial.
+ rewrite mult_IZR;ring[IHn].
+Qed.
+
 (**********)
 Lemma Ropp_Ropp_IZR : forall n:Z, IZR (- n) = - IZR n.
 Proof.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index f9ba589e..330c0042 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Rdefinitions.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rdefinitions.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 
 (*********************************************************)
@@ -55,6 +55,8 @@ Definition Rminus (r1 r2:R) : R := (r1 + - r2)%R.
 (**********)
 Definition Rdiv (r1 r2:R) : R := (r1 * / r2)%R.
 
+(**********)
+
 Infix "-" := Rminus : R_scope.
 Infix "/" := Rdiv : R_scope.
 
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index c727623c..3d1c0375 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rfunctions.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: Rfunctions.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 (*i Some properties about pow and sum have been made with John Harrison i*)
 (*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*)
@@ -15,10 +15,10 @@
 (**          Definition of the sum functions            *)
 (*                                                      *)
 (********************************************************)
-Require Export LegacyArithRing. (* for ring_nat... *)
 Require Export ArithRing.
 
 Require Import Rbase.
+Require Export Rpow_def.
 Require Export R_Ifp.
 Require Export Rbasic_fun.
 Require Export R_sqr.
@@ -65,11 +65,6 @@ Qed.
 (** *       Power              *)
 (*******************************)
 (*********)
-Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R :=
-  match n with
-    | O => 1
-    | S n => r * pow r n
-  end.
 
 Infix "^" := pow : R_scope.
 
@@ -382,7 +377,7 @@ Proof.
   replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)).
   rewrite Hrecn; reflexivity.
   simpl in |- *; ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n.
@@ -429,7 +424,7 @@ Proof.
   rewrite Hrecn2.
   simpl in |- *.
   ring.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma pow_incr : forall (x y:R) (n:nat), 0 <= x <= y -> x ^ n <= y ^ n.
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
new file mode 100644
index 00000000..5bdbb76b
--- /dev/null
+++ b/theories/Reals/Rpow_def.v
@@ -0,0 +1,7 @@
+Require Import Rdefinitions.
+
+Fixpoint pow (r:R) (n:nat) {struct n} : R :=
+  match n with
+    | O => R1
+    | S n => Rmult r (pow r n)
+  end.
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 690c420f..cb31d3b2 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rsigma.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rsigma.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -53,7 +53,7 @@ Section Sigma.
     apply lt_minus_O_lt; assumption.
     apply sum_eq; intros; replace (S k + S i)%nat with (S (S k) + i)%nat.
     reflexivity.
-    ring_nat.
+    ring.
     replace (high - S (S k))%nat with (high - S k - 1)%nat.
     apply pred_of_minus.
     omega.
@@ -71,7 +71,7 @@ Section Sigma.
     apply le_lt_trans with (S k); [ rewrite H2; apply le_n | assumption ].
     apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat.
     reflexivity.
-    ring_nat.
+    ring.
     omega.
     inversion H; [ right; reflexivity | left; assumption ].
   Qed.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 92284e7d..0a9f7754 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rsqrt_def.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rsqrt_def.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Sumbool.
 Require Import Rbase.
@@ -522,7 +522,7 @@ Proof.
   intro; assumption.
   intro; reflexivity.
   split.
-  intro; elim diff_false_true; assumption.
+  intro feqt;discriminate feqt.
   intro.
   elim n0; assumption.
   unfold Vn in |- *.
@@ -540,7 +540,7 @@ Proof.
   unfold cond_positivity in |- *.
   case (Rle_dec 0 z); intro.
   split.
-  intro; elim diff_true_false; assumption.
+  intro feqt; discriminate feqt.
   intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H7)).
   split.
   intro; auto with real.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 6e992aa3..b744c788 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rtrigo.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -466,10 +466,10 @@ Proof.
   unfold x in |- *; replace 0 with (INR 0);
     [ apply le_INR; apply le_O_n | reflexivity ].
   prove_sup0.
-  ring_nat.
+  ring.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  ring_nat.
+  ring.
 Qed.
 
 Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a.
@@ -1580,10 +1580,14 @@ Lemma cos_eq_0_0 :
 Proof.
   intros x H; rewrite cos_sin in H; generalize (sin_eq_0_0 (PI / INR 2 + x) H);
     intro H2; elim H2; intros x0 H3; exists (x0 - Z_of_nat 1)%Z;
-      rewrite <- Z_R_minus; simpl; ring_simplify;
-(* rewrite (Rmult_comm PI);*) (* old ring compat *)
+      rewrite <- Z_R_minus; simpl.
+unfold INR in H3. field_simplify [(sym_eq H3)]. field.
+(** 
+  ring_simplify.
+ (* rewrite (Rmult_comm PI);*) (* old ring compat *)
         rewrite <- H3; simpl;
-          field; repeat split; discrR.
+          field;repeat split; discrR.
+*)
 Qed.
 
 Lemma cos_eq_0_1 :
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index a95bc54b..89ee1745 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_alt.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rtrigo_alt.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -121,7 +121,7 @@ Proof.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   assert (H3 := cv_speed_pow_fact a); unfold Un in |- *; unfold Un_cv in H3;
     unfold R_dist in H3; unfold Un_cv in |- *; unfold R_dist in |- *; 
       intros; elim (H3 eps H4); intros N H5.
@@ -316,7 +316,7 @@ Proof.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   assert (H4 := cv_speed_pow_fact a0); unfold Un in |- *; unfold Un_cv in H4;
     unfold R_dist in H4; unfold Un_cv in |- *; unfold R_dist in |- *; 
       intros; elim (H4 eps H5); intros N H6; exists N; intros.
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 854c0b4a..b105ca69 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rtrigo_reg.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rtrigo_reg.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -99,7 +99,7 @@ Proof.
   apply pow_nonzero; assumption.
   replace (2 * S n)%nat with (S (S (2 * n))).
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rabs_no_R0; apply pow_nonzero; assumption.
@@ -280,7 +280,7 @@ Proof.
   apply pow_nonzero; assumption.
   replace (2 * S n)%nat with (S (S (2 * n))).
   simpl in |- *; ring.
-  ring_nat.
+  ring.
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rle_ge; apply pow_le; left; apply (cond_pos r).
   apply Rabs_no_R0; apply pow_nonzero; assumption.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 133f2b89..96351618 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: SeqProp.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: SeqProp.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -1265,8 +1265,8 @@ Proof.
   apply lt_le_trans with 1%nat; [ apply lt_O_Sn | assumption ].
   apply INR_fact_neq_0.
   apply not_O_INR; discriminate.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   unfold Vn in |- *; rewrite Rmult_assoc; unfold Rdiv in |- *;
     rewrite (Rmult_comm (Un 0%nat)); rewrite (Rmult_comm (Un n)).
   repeat apply Rmult_le_compat_l.
@@ -1293,8 +1293,8 @@ Proof.
   apply le_INR; omega.
   apply INR_fact_neq_0.
   apply INR_fact_neq_0.
-  ring_nat.
-  ring_nat.
+  ring.
+  ring.
   intro; unfold Un in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat.
   apply pow_lt; assumption.
   apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 40fd8f36..7e202359 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Operators_Properties.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Operators_Properties.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
 
 (****************************************************************************)
 (*                            Bruno Barras                                  *)
@@ -18,7 +18,7 @@ Require Import Relation_Operators.
 
 Section Properties.
 
-  Variable A : Set.
+  Variable A : Type.
   Variable R : relation A.
 
   Let incl (R1 R2:relation A) : Prop := forall x y:A, R1 x y -> R2 x y.
@@ -43,7 +43,7 @@ Section Properties.
     Qed.
 
     Lemma clos_refl_trans_ind_left :
-      forall (A:Set) (R:A -> A -> Prop) (M:A) (P:A -> Prop),
+      forall (A:Type) (R:A -> A -> Prop) (M:A) (P:A -> Prop),
 	P M ->
 	(forall P0 N:A, clos_refl_trans A R M P0 -> P P0 -> R P0 N -> P N) ->
 	forall a:A, clos_refl_trans A R M a -> P a.
@@ -95,4 +95,4 @@ Section Properties.
   
   End Clos_Refl_Sym_Trans.
 
-End Properties.
\ No newline at end of file
+End Properties.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 089246da..4c5a6519 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Relation_Operators.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Relation_Operators.v 9610 2007-02-07 14:45:18Z herbelin $ i*)
 
 (****************************************************************************)
 (*                      Bruno Barras, Cristina Cornes                       *)
@@ -78,7 +78,7 @@ End Union.
 
 
 Section Disjoint_Union.
-Variables A B : Set.
+Variables A B : Type.
 Variable leA : A -> A -> Prop.
 Variable leB : B -> B -> Prop.
 
@@ -94,8 +94,8 @@ End Disjoint_Union.
 Section Lexicographic_Product.
   (* Lexicographic order on dependent pairs *)
 
-  Variable A : Set.
-  Variable B : A -> Set.
+  Variable A : Type.
+  Variable B : A -> Type.
   Variable leA : A -> A -> Prop.
   Variable leB : forall x:A, B x -> B x -> Prop.
 
@@ -110,8 +110,8 @@ End Lexicographic_Product.
 
 
 Section Symmetric_Product.
-  Variable A : Set.
-  Variable B : Set.
+  Variable A : Type.
+  Variable B : Type.
   Variable leA : A -> A -> Prop.
   Variable leB : B -> B -> Prop.
 
@@ -125,7 +125,7 @@ End Symmetric_Product.
 
 
 Section Swap.
-  Variable A : Set.
+  Variable A : Type.
   Variable R : A -> A -> Prop.
 
   Inductive swapprod : A * A -> A * A -> Prop :=
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 9b2f4057..9da30e9b 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Relations.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Relations.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
 
 Require Export Relation_Definitions.
 Require Export Relation_Operators.
 Require Export Operators_Properties.
 
 Lemma inverse_image_of_equivalence :
-  forall (A B:Set) (f:A -> B) (r:relation B),
+  forall (A B:Type) (f:A -> B) (r:relation B),
     equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
 Proof.
   intros; split; elim H; red in |- *; auto.
@@ -21,7 +21,7 @@ Proof.
 Qed.
 
 Lemma inverse_image_of_eq :
-  forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y).
+  forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y).
 Proof.
   split; red in |- *;
     [  (* reflexivity *) reflexivity
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 24816a20..efdf0495 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Lexicographic_Exponentiation.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Lexicographic_Exponentiation.v 9610 2007-02-07 14:45:18Z herbelin $ i*)
 
 (** Author: Cristina Cornes
 
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 8ac0d546..051c8127 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Lexicographic_Product.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Lexicographic_Product.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
 
 (** Authors: Bruno Barras, Cristina Cornes *)
 
@@ -18,8 +18,8 @@ Require Import Transitive_Closure.
      L. Paulson  JSC (1986) 2, 325-355 *)
 
 Section WfLexicographic_Product.
-  Variable A : Set.
-  Variable B : A -> Set.
+  Variable A : Type.
+  Variable B : A -> Type.
   Variable leA : A -> A -> Prop.
   Variable leB : forall x:A, B x -> B x -> Prop.
 
@@ -74,8 +74,8 @@ End WfLexicographic_Product.
 
 
 Section Wf_Symmetric_Product.
-  Variable A : Set.
-  Variable B : Set.
+  Variable A : Type.
+  Variable B : Type.
   Variable leA : A -> A -> Prop.
   Variable leB : B -> B -> Prop.
 
@@ -106,7 +106,7 @@ End Wf_Symmetric_Product.
 
 Section Swap.
   
-  Variable A : Set.
+  Variable A : Type.
   Variable R : A -> A -> Prop.
 
   Notation SwapProd := (swapprod A R).
@@ -168,4 +168,4 @@ Section Swap.
     apply Acc_swapprod; auto with sets.
   Qed.
 
-End Swap.
\ No newline at end of file
+End Swap.
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 5bf82ffb..bd4e4fec 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Transitive_Closure.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: Transitive_Closure.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
 
 (** Author: Bruno Barras *)
 
@@ -14,7 +14,7 @@ Require Import Relation_Definitions.
 Require Import Relation_Operators.
 
 Section Wf_Transitive_Closure.
-  Variable A : Set.
+  Variable A : Type.
   Variable R : relation A.
 
   Notation trans_clos := (clos_trans A R).
@@ -44,4 +44,4 @@ Section Wf_Transitive_Closure.
     unfold well_founded in |- *; auto with sets.
   Qed.
 
-End Wf_Transitive_Closure.
\ No newline at end of file
+End Wf_Transitive_Closure.
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index 69617de2..f691f2b7 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Well_Ordering.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Well_Ordering.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
 
 (** Author: Cristina Cornes.
     From: Constructing Recursion Operators in Type Theory
@@ -15,10 +15,10 @@
 Require Import Eqdep.
 
 Section WellOrdering.
-  Variable A : Set.
-  Variable B : A -> Set. 
+  Variable A : Type.
+  Variable B : A -> Type. 
   
-  Inductive WO : Set :=
+  Inductive WO : Type :=
     sup : forall (a:A) (f:B a -> WO), WO.
 
 
@@ -52,7 +52,7 @@ Section Characterisation_wf_relations.
   (*  in course of development                                          *)
 
 
-  Variable A : Set.
+  Variable A : Type.
   Variable leA : A -> A -> Prop.
 
   Definition B (a:A) := {x : A | leA x a}.
@@ -60,12 +60,12 @@ Section Characterisation_wf_relations.
   Definition wof : well_founded leA -> A -> WO A B.
   Proof.
     intros.
-    apply (well_founded_induction H (fun a:A => WO A B)); auto.
-    intros.
+    apply (well_founded_induction_type H (fun a:A => WO A B)); auto.
+    intros x H1.
     apply (sup A B x).
     unfold B at 1 in |- *.
     destruct 1 as [x0].
     apply (H1 x0); auto.
 Qed.
 
-End Characterisation_wf_relations.
\ No newline at end of file
+End Characterisation_wf_relations.
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v
new file mode 100644
index 00000000..b0f372de
--- /dev/null
+++ b/theories/ZArith/Zpow_def.v
@@ -0,0 +1,27 @@
+Require Import ZArith_base.
+Require Import Ring_theory.
+
+Open Local Scope Z_scope.
+ 
+(** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
+      integer (type [positive]) and [z] a signed integer (type [Z]) *) 
+Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1.
+  
+Definition Zpower (x y:Z) :=
+    match y with
+      | Zpos p => Zpower_pos x p
+      | Z0 => 1
+      | Zneg p => 0
+    end.
+
+Lemma Zpower_theory : power_theory 1 Zmult (eq (A:=Z)) Z_of_N Zpower.
+Proof.
+ constructor. intros.
+ destruct n;simpl;trivial.
+ unfold Zpower_pos.
+ assert (forall k, iter_pos p Z (fun x : Z => r * x) k = pow_pos Zmult r p*k).
+ induction p;simpl;intros;repeat rewrite IHp;trivial;
+   repeat rewrite Zmult_assoc;trivial.
+ rewrite H;rewrite Zmult_1_r;trivial.
+Qed.
+ 
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 446f663c..c9cee31d 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -6,9 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zpower.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Zpower.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
 
 Require Import ZArith_base.
+Require Export Zpow_def.
 Require Import Omega.
 Require Import Zcomplements.
 Open Local Scope Z_scope.
@@ -35,11 +36,6 @@ Section section1.
 	  apply Zmult_assoc ].
   Qed.
 
-  (** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
-      integer (type [positive]) and [z] a signed integer (type [Z]) *) 
-
-  Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1.
-
   (** This theorem shows that powers of unary and binary integers
      are the same thing, modulo the function convert : [positive -> nat] *)
 
@@ -66,13 +62,6 @@ Section section1.
     apply Zpower_nat_is_exp.
   Qed.
 
-  Definition Zpower (x y:Z) :=
-    match y with
-      | Zpos p => Zpower_pos x p
-      | Z0 => 1
-      | Zneg p => 0
-    end.
-
   Infix "^" := Zpower : Z_scope.
 
   Hint Immediate Zpower_nat_is_exp: zarith.
@@ -382,4 +371,4 @@ Section power_div_with_rest.
       apply Zdiv_rest_proof with (q := a0) (r := b); assumption.
   Qed.
 
-End power_div_with_rest.
\ No newline at end of file
+End power_div_with_rest.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 9893bed3..3f475a63 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Zsqrt.v 9245 2006-10-17 12:53:34Z notin $ *)
+(* $Id: Zsqrt.v 9551 2007-01-29 15:13:35Z bgregoir $ *)
 
 Require Import ZArithRing.
 Require Import Omega.
@@ -132,7 +132,7 @@ Definition Zsqrt :
                (fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0
                _)
     end); try omega.
-split; [ omega | rewrite Heq; ring_simplify ((s + 1) * (s + 1)); omega ].
+ split; [ omega | rewrite Heq; ring_simplify (s*s) ((s + 1) * (s + 1)); omega ].
 Defined.
 
 (** Define a function of type Z->Z that computes the integer square root,