Suppression d'Export redondants

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

5 files changed, 10 insertions, 10 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 645f4b0d7..0bf52ee2e 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Export Datatypes.
+Require Datatypes.
 
 (* [True] is the always true proposition *)
 Inductive True : Prop := I : True. 
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index dcfbe5e99..9134127be 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -21,9 +21,9 @@
    including Peano's axioms of arithmetic (in Coq, these are in fact provable)
    Case analysis on [nat] and induction on [nat * nat] are provided too *)
 
-Require Export Logic.
-Require Export LogicSyntax.
-Require Export Datatypes.
+Require Logic.
+Require LogicSyntax.
+Require Datatypes.
 
 Definition eq_S := (f_equal nat nat S).
 
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 3bbb9ba7e..135f0f727 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -12,9 +12,9 @@
 (* Basic specifications : Sets containing logical information *)
 (**************************************************************)
 
-Require Export Logic.
-Require LogicSyntax.
 Require Datatypes.
+Require Logic.
+Require LogicSyntax.
 
 Section Subsets.
 
diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v
index 1f4d0278e..f732ced89 100644
--- a/theories/Init/SpecifSyntax.v
+++ b/theories/Init/SpecifSyntax.v
@@ -8,8 +8,8 @@
 
 (* $Id$ *)
 
-Require Export LogicSyntax.
-Require Export Specif.
+Require LogicSyntax.
+Require Specif.
 
 (* Parsing of things in Specif.v *)
 
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index bd55dcd1d..87d5c720d 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -13,8 +13,8 @@
     - well-founded induction
    from a well-founded ordering on a given set *)
 
-Require Export Logic.
-Require Export LogicSyntax.
+Require Logic.
+Require LogicSyntax.
 
 (* Well-founded induction principle on Prop *)