From 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 29 Nov 2003 17:28:49 +0000
Subject: 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
---
 theories/ZArith/ZArith_base.v | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

(limited to 'theories/ZArith/ZArith_base.v')

diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 97f4c3f3ed..ec57dda578 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -12,10 +12,6 @@
     These are the basic modules, required by [Omega] and [Ring] for instance. 
     The full library is [ZArith]. *)
 
-V7only [
-Require Export fast_integer.
-Require Export zarith_aux.
-].
 Require Export BinPos.
 Require Export BinNat.
 Require Export BinInt.
@@ -26,14 +22,13 @@ Require Export Zmin.
 Require Export Zabs.
 Require Export Znat.
 Require Export auxiliary.
-Require Export Zsyntax.
 Require Export ZArith_dec.
 Require Export Zbool.
 Require Export Zmisc.
 Require Export Wf_Z.
 
-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.
+Require Export Zhints.
\ No newline at end of file
-- 
cgit v1.2.3