Renoncement de la compatibilite des noms qualifies au profit de la compatibilite des arguments implicites

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

1 files changed, 0 insertions, 24 deletions

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 2fb544cf5..8d27f81d2 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -210,27 +210,3 @@ End Zlength_properties.
 Implicits Zlength_correct [1].
 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.
-].