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

1 files changed, 30 insertions, 3 deletions

diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v
index 13896123be..92fbc1b587 100644
--- a/contrib/setoid_ring/RealField.v
+++ b/contrib/setoid_ring/RealField.v
@@ -1,6 +1,9 @@
-Require Import Raxioms.
-Require Import Rdefinitions.
+Require Import Nnat.
+Require Import ArithRing. 
 Require Export Ring Field.
+Require Import Rdefinitions.
+Require Import Rpow_def.
+Require Import Raxioms.
 
 Open Local Scope R_scope.
 
@@ -102,4 +105,28 @@ Lemma Zeq_bool_complete : forall x y,
   Zeq_bool x y = true.
 Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0.
 
-Add Field RField : Rfield (infinite Zeq_bool_complete).
+Lemma Rdef_pow_add : forall (x:R) (n m:nat), pow x  (n + m) = pow x n * pow x m.
+Proof.
+  intros x n; elim n; simpl in |- *; auto with real.
+  intros n0 H' m; rewrite H'; auto with real.
+Qed.
+
+Lemma R_power_theory : power_theory 1%R Rmult (eq (A:=R))  nat_of_N pow.
+Proof.
+ constructor. destruct n. reflexivity.
+ simpl. induction p;simpl. 
+ rewrite ZL6. rewrite Rdef_pow_add;rewrite IHp. symmetry; apply Rmult_assoc.
+ unfold nat_of_P;simpl;rewrite ZL6;rewrite Rdef_pow_add;rewrite IHp;trivial.
+ rewrite Rmult_comm;apply Rmult_1_l.
+Qed.
+
+Ltac Rpow_tac t := 
+  match isnatcst t with
+  | false => constr:(InitialRing.NotConstant)
+  | _ => constr:(N_of_nat t)
+  end. 
+
+Add Field RField : Rfield  (infinite Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]).
+
+
+