Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

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

1 files changed, 28 insertions, 28 deletions

diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 480f7594be..e381b1fbeb 100755
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -19,9 +19,9 @@
 Require Export ZArith_base.
 Require Export OmegaLemmas.
 
-Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc
-  Zero_left Zero_right Zmult_one Zplus_inverse_l Zplus_inverse_r 
-  Zmult_plus_distr_l Zmult_plus_distr_r : zarith.
+Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
+  Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
+  Zmult_plus_distr_r: zarith.
 
 Require Export Zhints.
 
@@ -30,28 +30,28 @@ Require Export Zhints.
 Require Minus.
 *)
 
-Hint eq_nat_Omega : zarith := Extern 10 (eq nat ? ?) Abstract Omega.
-Hint le_Omega : zarith := Extern 10 (le ? ?) Abstract Omega.
-Hint lt_Omega : zarith := Extern 10 (lt ? ?) Abstract Omega.
-Hint ge_Omega : zarith := Extern 10 (ge ? ?) Abstract Omega.
-Hint gt_Omega : zarith := Extern 10 (gt ? ?) Abstract Omega.
-
-Hint not_eq_nat_Omega : zarith := Extern 10 ~(eq nat ? ?) Abstract Omega.
-Hint not_le_Omega : zarith := Extern 10 ~(le ? ?) Abstract Omega.
-Hint not_lt_Omega : zarith := Extern 10 ~(lt ? ?) Abstract Omega.
-Hint not_ge_Omega : zarith := Extern 10 ~(ge ? ?) Abstract Omega.
-Hint not_gt_Omega : zarith := Extern 10 ~(gt ? ?) Abstract Omega.
-
-Hint eq_Z_Omega : zarith := Extern 10 (eq Z ? ?) Abstract Omega.
-Hint Zle_Omega : zarith := Extern 10 (Zle ? ?) Abstract Omega.
-Hint Zlt_Omega : zarith := Extern 10 (Zlt ? ?) Abstract Omega.
-Hint Zge_Omega : zarith := Extern 10 (Zge ? ?) Abstract Omega.
-Hint Zgt_Omega : zarith := Extern 10 (Zgt ? ?) Abstract Omega.
-
-Hint not_eq_nat_Omega : zarith := Extern 10 ~(eq Z ? ?) Abstract Omega.
-Hint not_Zle_Omega : zarith := Extern 10 ~(Zle ? ?) Abstract Omega.
-Hint not_Zlt_Omega : zarith := Extern 10 ~(Zlt ? ?) Abstract Omega.
-Hint not_Zge_Omega : zarith := Extern 10 ~(Zge ? ?) Abstract Omega.
-Hint not_Zgt_Omega : zarith := Extern 10 ~(Zgt ? ?) Abstract Omega.
-
-Hint false_Omega : zarith := Extern 10 False Abstract Omega.
+Hint Extern 10 (_ = _ :>nat) => abstract omega: zarith.
+Hint Extern 10 (_ <= _) => abstract omega: zarith.
+Hint Extern 10 (_ < _) => abstract omega: zarith.
+Hint Extern 10 (_ >= _) => abstract omega: zarith.
+Hint Extern 10 (_ > _) => abstract omega: zarith.
+
+Hint Extern 10 (_ <> _ :>nat) => abstract omega: zarith.
+Hint Extern 10 (~ _ <= _) => abstract omega: zarith.
+Hint Extern 10 (~ _ < _) => abstract omega: zarith.
+Hint Extern 10 (~ _ >= _) => abstract omega: zarith.
+Hint Extern 10 (~ _ > _) => abstract omega: zarith.
+
+Hint Extern 10 (_ = _ :>Z) => abstract omega: zarith.
+Hint Extern 10 (_ <= _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ < _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ >= _)%Z => abstract omega: zarith.
+Hint Extern 10 (_ > _)%Z => abstract omega: zarith.
+
+Hint Extern 10 (_ <> _ :>Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ <= _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith.
+Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith.
+
+Hint Extern 10 False => abstract omega: zarith.
\ No newline at end of file