portage Omega (mais toujours pas Zpower et Zlogarithm)

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

5 files changed, 14 insertions, 49 deletions

diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 185a85969..13a764253 100755
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -6,6 +6,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* $Id$ *)
+
 Require Export ZArith.
 (* The constant minus is required in coq_omega.ml *)
 Require Export Minus.
diff --git a/contrib/omega/OmegaSyntax.v b/contrib/omega/OmegaSyntax.v
index dccfc5e89..4028a1efb 100644
--- a/contrib/omega/OmegaSyntax.v
+++ b/contrib/omega/OmegaSyntax.v
@@ -6,6 +6,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* $Id$ *)
+
 Grammar vernac vernac :=
   omega_sett [ "Set" "Omega" "Time" "." ] -> [(OmegaFlag "+time")]
 | omega_sets [ "Set" "Omega" "System" "." ] -> [(OmegaFlag "+system")]
diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v
index 6bf081781..1cbf284a5 100644
--- a/contrib/omega/Zcomplements.v
+++ b/contrib/omega/Zcomplements.v
@@ -1,18 +1,7 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(*                              Zcomplements.v                              *)
-(****************************************************************************)
 
+(* $Id$ *)
+
+Require ZArith.
 Require Omega.
 Require Wf_nat.
 
@@ -95,7 +84,7 @@ Simpl; Do 2 Rewrite Zmult_n_1; Auto 1.
 Unfold Zs.
 Intros x0 Hx0; Repeat (Rewrite Zmult_plus_distr_r).
 Repeat Rewrite Zmult_n_1.
-Auto with zarith.
+Omega.
 Unfold Zpred; Omega.
 Save.
 
@@ -308,6 +297,3 @@ Destruct a;
 Save.
 
 End diveucl.
-
-(* $Id$ *)
-
diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v
index 87f1f87c5..c5b36397f 100644
--- a/contrib/omega/Zlogarithm.v
+++ b/contrib/omega/Zlogarithm.v
@@ -1,17 +1,5 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(*                              Zlogarithm.v                                *)
-(****************************************************************************)
+
+(* $Id$ *)
 
 (****************************************************************************)
 (*  The integer logarithms with base 2. There are three logarithms,	    *)
diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v
index 475638ce2..d56e607d5 100644
--- a/contrib/omega/Zpower.v
+++ b/contrib/omega/Zpower.v
@@ -1,18 +1,7 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
-(*              Rocquencourt         Orsay          Lyon                    *)
-(*                                                                          *)
-(*                                 Coq V6.3                                 *)
-(*                               July 1st 1999                              *)
-(*                                                                          *)
-(****************************************************************************)
-(*                                  Zpower.v                                *)
-(****************************************************************************)
 
+(* $Id$ *)
+
+Require ZArith.
 Require Omega.
 Require Zcomplements.
 
@@ -82,7 +71,7 @@ Hints Unfold  Zpower_nat : zarith.
 
 Lemma Zpower_exp : (x:Z)(n,m:Z)
   `n >= 0` -> `m >= 0` -> `(Zpower x (n+m))=(Zpower x n)*(Zpower x m)`.
-Destruct n;  Destruct m; Auto with zarith.
+Destruct n; Destruct m; Auto with zarith.
 Simpl; Intros; Apply Zred_factor0.
 Simpl; Auto with zarith.
 Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith.
@@ -392,5 +381,3 @@ Apply Zdiv_rest_proof with q:=y0 r:=y1; Assumption.
 Save.
 
 End power_div_with_rest.
-
-