Compatibilite

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

4 files changed, 167 insertions, 10 deletions

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 85e062ebc..2fb544cf5 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -15,11 +15,6 @@ Require Wf_nat.
 V7only [Import Z_scope.].
 Open Local Scope Z_scope.
 
-V7only [
-Notation Zcompare_Zmult_right := Zcompare_Zmult_right.
-Notation Zcompare_Zmult_left := Zcompare_Zmult_left.
-].
-
 V7only [Set Implicit Arguments.].
 
 (**********************************************************************)
@@ -217,3 +212,25 @@ Implicits Zlength_cons [1].
 Implicits Zlength_nil_inv [1].
 
 (**********************************************************************)
+V7only [
+(* Compatibility *)
+Notation Zcompare_Zmult_right := Zcompare_Zmult_right.
+Notation Zcompare_Zmult_left := Zcompare_Zmult_left.
+Notation Zmult_zero := Zmult_zero.
+Notation Zeq_Zminus := Zeq_Zminus.
+Notation Zminus_Zeq := Zminus_Zeq.
+Notation Zmult_Zminus_distr_l := Zmult_Zminus_distr_l.
+Notation Zmult_reg_left := Zmult_reg_left.
+Notation Zmult_reg_right := Zmult_reg_right.
+Notation Zgt0_le_pred := Zgt0_le_pred.
+Notation Zlt_Zplus := Zlt_Zplus.
+Notation Zlt_Zmult_right := Zlt_Zmult_right.
+Notation Zlt_Zmult_right2 := Zlt_Zmult_right2.
+Notation Zle_Zmult_right := Zle_Zmult_right.
+Notation Zle_Zmult_right2 := Zle_Zmult_right2.
+Notation Zgt_Zmult_right := Zgt_Zmult_right.
+Notation Zlt_Zmult_left := Zlt_Zmult_left.
+Notation Zgt_Zmult_left := Zgt_Zmult_left.
+Export BinInt.
+Export Zorder.
+].
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 42f461857..a8bbcfc00 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -99,5 +99,90 @@ Proof.
 Intros; Rewrite iter_convert; Apply iter_nat_invariant; Trivial with arith.
 Qed.
 
-
-
+V7only [
+(* Compatibility *)
+Require Zbool.
+Require Zeven.
+Require Zabs.
+Require Zmin.
+Notation rename := rename.
+Notation POS_xI := POS_xI.
+Notation POS_xO := POS_xO.
+Notation NEG_xI := NEG_xI.
+Notation NEG_xO := NEG_xO.
+Notation POS_add := POS_add.
+Notation NEG_add := NEG_add.
+Notation Zle_cases := Zle_cases.
+Notation Zlt_cases := Zlt_cases.
+Notation Zge_cases := Zge_cases.
+Notation Zgt_cases := Zgt_cases.
+Notation POS_gt_ZERO := POS_gt_ZERO.
+Notation ZERO_le_POS := ZERO_le_POS.
+Notation Zlt_ZERO_pred_le_ZERO := Zlt_ZERO_pred_le_ZERO.
+Notation NEG_lt_ZERO := NEG_lt_ZERO.
+Notation Zeven_not_Zodd := Zeven_not_Zodd.
+Notation Zodd_not_Zeven := Zodd_not_Zeven.
+Notation Zeven_Sn := Zeven_Sn.
+Notation Zodd_Sn := Zodd_Sn.
+Notation Zeven_pred := Zeven_pred.
+Notation Zodd_pred := Zodd_pred.
+Notation Zeven_div2 := Zeven_div2.
+Notation Zodd_div2 := Zodd_div2.
+Notation Zodd_div2_neg := Zodd_div2_neg.
+Notation Z_modulo_2 := Z_modulo_2.
+Notation Zsplit2 := Zsplit2.
+Notation Zminus_Zplus_compatible := Zminus_Zplus_compatible.
+Notation Zcompare_egal_dec := Zcompare_egal_dec.
+Notation Zcompare_elim := Zcompare_elim.
+Notation Zcompare_x_x := Zcompare_x_x.
+Notation Zlt_not_eq := Zlt_not_eq.
+Notation Zcompare_eq_case := Zcompare_eq_case.
+Notation Zle_Zcompare := Zle_Zcompare.
+Notation Zlt_Zcompare := Zlt_Zcompare.
+Notation Zge_Zcompare := Zge_Zcompare.
+Notation Zgt_Zcompare := Zgt_Zcompare.
+Notation Zmin_plus := Zmin_plus.
+Notation absolu_lt := absolu_lt.
+Notation Zle_bool_imp_le := Zle_bool_imp_le.
+Notation Zle_imp_le_bool := Zle_imp_le_bool.
+Notation Zle_bool_refl := Zle_bool_refl.
+Notation Zle_bool_antisym := Zle_bool_antisym.
+Notation Zle_bool_trans := Zle_bool_trans.
+Notation Zle_bool_plus_mono := Zle_bool_plus_mono.
+Notation Zone_pos := Zone_pos.
+Notation Zone_min_pos := Zone_min_pos.
+Notation Zle_is_le_bool := Zle_is_le_bool.
+Notation Zge_is_le_bool := Zge_is_le_bool.
+Notation Zlt_is_le_bool := Zlt_is_le_bool.
+Notation Zgt_is_le_bool := Zgt_is_le_bool.
+Notation Zle_plus_swap := Zle_plus_swap.
+Notation Zge_iff_le := Zge_iff_le.
+Notation Zlt_plus_swap := Zlt_plus_swap.
+Notation Zgt_iff_lt := Zgt_iff_lt.
+Notation Zeq_plus_swap := Zeq_plus_swap.
+(* Definitions *)
+Notation entier_of_Z := entier_of_Z.
+Notation Z_of_entier := Z_of_entier.
+Notation Zle_bool := Zle_bool.
+Notation Zge_bool := Zge_bool.
+Notation Zlt_bool := Zlt_bool.
+Notation Zgt_bool := Zgt_bool.
+Notation Zeq_bool := Zeq_bool.
+Notation Zneq_bool := Zneq_bool.
+Notation Zeven := Zeven.
+Notation Zodd := Zodd.
+Notation Zeven_bool := Zeven_bool.
+Notation Zodd_bool := Zodd_bool.
+Notation Zeven_odd_dec := Zeven_odd_dec.
+Notation Zeven_dec := Zeven_dec.
+Notation Zodd_dec := Zodd_dec.
+Notation Zdiv2_pos := Zdiv2_pos.
+Notation Zdiv2 := Zdiv2.
+Notation Zle_bool_total := Zle_bool_total.
+Export Zbool.
+Export Zeven.
+Export Zabs.
+Export Zmin.
+Export Zorder.
+Export Zcompare.
+].
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index e5ee2682d..b8040335e 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -8,9 +8,9 @@
 
 (* $Id$ *)
 
+Require Omega.
 Require Export ZArith_base.
 Require Export ZArithRing.
-Require Export Omega.
 V7only [Import Z_scope.].
 Open Local Scope Z_scope.
 
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index 0d5becb59..3f713c5ed 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -160,5 +160,60 @@ Intros x y z H1 H2 H3; Apply Zlt_n_Sm_le; Apply Zmult_lt with x; [
 
 Qed.
 
-V7only [Notation OMEGA2 := Zle_0_plus.].
-
+V7only [
+(* Compatibility *)
+Require Znat.
+Require Zcompare.
+Notation neq := neq.
+Notation Zne := Zne.
+Notation OMEGA2 := Zle_0_plus.
+Notation add_un_Zs := add_un_Zs.
+Notation inj_S := inj_S.
+Notation Zplus_S_n := Zplus_S_n.
+Notation inj_plus := inj_plus.
+Notation inj_mult := inj_mult.
+Notation inj_neq := inj_neq.
+Notation inj_le := inj_le.
+Notation inj_lt := inj_lt.
+Notation inj_gt := inj_gt.
+Notation inj_ge := inj_ge.
+Notation inj_eq := inj_eq.
+Notation intro_Z := intro_Z.
+Notation inj_minus1 := inj_minus1.
+Notation inj_minus2 := inj_minus2.
+Notation dec_eq := dec_eq.
+Notation dec_Zne := dec_Zne.
+Notation dec_Zle := dec_Zle.
+Notation dec_Zgt := dec_Zgt.
+Notation dec_Zge := dec_Zge.
+Notation dec_Zlt := dec_Zlt.
+Notation dec_eq_nat := dec_eq_nat.
+Notation not_Zge := not_Zge.
+Notation not_Zlt := not_Zlt.
+Notation not_Zle := not_Zle.
+Notation not_Zgt := not_Zgt.
+Notation not_Zeq := not_Zeq.
+Notation Zopp_one := Zopp_one.
+Notation Zopp_Zmult_r := Zopp_Zmult_r.
+Notation Zmult_Zopp_left := Zmult_Zopp_left.
+Notation Zopp_Zmult_l := Zopp_Zmult_l.
+Notation Zcompare_Zplus_compatible2 := Zcompare_Zplus_compatible2.
+Notation Zcompare_Zmult_compatible := Zcompare_Zmult_compatible.
+Notation Zmult_eq := Zmult_eq.
+Notation Z_eq_mult := Z_eq_mult.
+Notation Zmult_le := Zmult_le.
+Notation Zle_ZERO_mult := Zle_ZERO_mult.
+Notation Zgt_ZERO_mult := Zgt_ZERO_mult.
+Notation Zle_mult := Zle_mult.
+Notation Zmult_lt := Zmult_lt.
+Notation Zmult_gt := Zmult_gt.
+Notation Zle_Zmult_pos_right := Zle_Zmult_pos_right.
+Notation Zle_Zmult_pos_left := Zle_Zmult_pos_left.
+Notation Zge_Zmult_pos_right := Zge_Zmult_pos_right.
+Notation Zge_Zmult_pos_left := Zge_Zmult_pos_left.
+Notation Zge_Zmult_pos_compat := Zge_Zmult_pos_compat.
+Notation Zle_mult_simpl := Zle_mult_simpl.
+Notation Zge_mult_simpl := Zge_mult_simpl.
+Notation Zgt_mult_simpl := Zgt_mult_simpl.
+Notation Zgt_square_simpl := Zgt_square_simpl.
+].