From 9772d55236a9d87218b4eb9e261e41cb3cf4c4af Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Nov 2003 15:07:03 +0000
Subject: Quelques oublis pour que les notations marchent bien

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4907 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/fast_integer.v | 7 +++----
 theories/ZArith/zarith_aux.v   | 6 +++++-
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 2c8969a810..81b69037f8 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -16,6 +16,7 @@ Require BinPos.
 Require BinNat.
 Require BinInt.
 Require Zcompare.
+Require Mult.
 
 V7only [
 (* Defs and ppties on positive, entier and Z, previously in fast_integer *)
@@ -80,10 +81,7 @@ Notation simpl_add_carry_r := simpl_add_carry_r.
 Notation simpl_add_l := simpl_add_l.
 Notation simpl_add_carry_l := simpl_add_carry_l.
 Notation add_assoc := add_assoc.
-Notation xO_xI_plus_double_moins_un := xO_xI_plus_double_moins_un.
-Notation double_moins_un_plus_xO_double_moins_un := double_moins_un_plus_xO_double_moins_un.
 Notation add_xI_double_moins_un := add_xI_double_moins_un.
-Notation double_moins_un_add := double_moins_un_add.
 Notation add_x_x := add_x_x.
 Notation ZS := ZS.
 Notation US := US.
@@ -168,7 +166,7 @@ Notation Zplus_simpl := Zplus_simpl.
 Notation Zmult_sym := Zmult_sym.
 Notation Zmult_assoc := Zmult_assoc.
 Notation Zmult_one := Zmult_one.
-Notation lt_mult_left := lt_mult_left.
+Notation lt_mult_left := lt_mult_left. (* Mult*)
 Notation Zero_mult_left := Zero_mult_left.
 Notation Zero_mult_right := Zero_mult_right.
 Notation Zopp_Zmult := Zopp_Zmult.
@@ -189,4 +187,5 @@ Export BinPos.
 Export BinNat.
 Export BinInt.
 Export Zcompare.
+Export Mult.
 ].
diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v
index 72a57d0fb0..61a712b92f 100644
--- a/theories/ZArith/zarith_aux.v
+++ b/theories/ZArith/zarith_aux.v
@@ -7,6 +7,8 @@
 (***********************************************************************)
 (*i $Id$ i*)
 
+Require Export BinInt.
+Require Export Zcompare.
 Require Export Zorder.
 Require Export Zmin.
 Require Export Zabs.
@@ -69,7 +71,7 @@ Notation Zle_refl := Zle_refl.
 Notation Zle_trans := Zle_trans.
 Notation Zle_n_Sn := Zle_n_Sn.
 Notation Zle_n_S := Zle_n_S.
-Notation Zs_pred := Zs_pred.
+Notation Zs_pred := Zs_pred. (* BinInt *)
 Notation Zle_pred_n := Zle_pred_n.
 Notation Zle_trans_S := Zle_trans_S.
 Notation Zle_Sn_n := Zle_Sn_n.
@@ -141,7 +143,9 @@ Notation Zmult_1_n := Zmult_1_n.
 Notation Zmult_n_1 := Zmult_n_1.
 Notation Zmult_Sm_n := Zmult_Sm_n.
 Notation Zmult_Zplus_distr := Zmult_plus_distr_r.
+Export BinInt.
 Export Zorder.
 Export Zmin.
 Export Zabs.
+Export Zcompare.
 ].
-- 
cgit v1.2.3