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, 2 insertions, 13 deletions

diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 248af0102..4e08c726e 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -9,6 +9,7 @@
 (*i $Id$ 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.