From c710be6c4d2fda836939c404a1795e8a9171634e Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 17 Feb 2010 13:44:32 +0000
Subject: Kill some useless dependencies (Bvector, Program.Syntax)

 Bvector uses only Minus, so let's avoid loading Arith
  (and hence ArithRing and hence parts of Z, N)
 Program.Syntax no longer need Lists now that list is in Datatypes.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12785 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Syntax.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'theories/Program/Syntax.v')

diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 2064977fef..916c33ee62 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -35,8 +35,6 @@ Implicit Arguments pair [[A] [B]].
 Implicit Arguments fst [[A] [B]].
 Implicit Arguments snd [[A] [B]].
 
-Require Import Coq.Lists.List.
-
 Implicit Arguments nil [[A]].
 Implicit Arguments cons [[A]].
 
-- 
cgit v1.2.3