Changement dans le kernel :

   - essai de suppression des dependances debiles. (echec) 
   - Application des patch debian.

Pour ring et field :
   - introduciton de la function de sign et de puissance.
   - Correction de certains bug.
   - supression de ring_replace ....

Pour exact_no_check :
   - ajout de la tactic : vm_cast_no_check (t)
     qui remplace "exact_no_check (t<: type of Goal)"
      (cette version forcais l'evaluation du cast dans le 
       pretypage).




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 27 insertions, 19 deletions

diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index a3dbca23d..eff4a6c3d 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -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/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 7077d1015..3447aa0e4 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -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 f048faf53..ba7396ed6 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -19,6 +19,7 @@ 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 +66,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.
 
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
new file mode 100644
index 000000000..5bdbb76b9
--- /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/Rtrigo.v b/theories/Reals/Rtrigo.v
index d05fd99cb..2adac468b 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -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 :