From 23202ec79d0b2ebc046810a37dfcce80c3aa8325 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 19:27:54 +0000
Subject: Suppression DatatypesSyntax et PeanoSyntax qui était vides

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4383 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/DatatypesSyntax.v | 10 ----------
 theories/Init/PeanoSyntax.v     | 12 ------------
 theories/Init/Prelude.v         |  2 --
 3 files changed, 24 deletions(-)
 delete mode 100644 theories/Init/DatatypesSyntax.v
 delete mode 100644 theories/Init/PeanoSyntax.v

diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v
deleted file mode 100644
index a4b6a57aae..0000000000
--- a/theories/Init/DatatypesSyntax.v
+++ /dev/null
@@ -1,10 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v
deleted file mode 100644
index 3b7b914542..0000000000
--- a/theories/Init/PeanoSyntax.v
+++ /dev/null
@@ -1,12 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-(*i 	$Id$ *)
-
-Require Datatypes.
-Require Peano.
-
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 51a62db8ee..972a809866 100755
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -10,11 +10,9 @@
 
 Require Export Notations.
 Require Export Datatypes.
-Require Export DatatypesSyntax.
 Require Export Logic.
 Require Export LogicSyntax.
 Require Export Specif.
 Require Export SpecifSyntax.
 Require Export Peano.
-Require Export PeanoSyntax.
 Require Export Wf.
-- 
cgit v1.2.3