diff options
| author | letouzey | 2010-02-17 13:44:32 +0000 |
|---|---|---|
| committer | letouzey | 2010-02-17 13:44:32 +0000 |
| commit | c710be6c4d2fda836939c404a1795e8a9171634e (patch) | |
| tree | f3e88e762686b03d7d3a98655a7e2f75db652846 | |
| parent | e9ccfc401c610ce4df6b06f48c611070a26f89d7 (diff) | |
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
| -rw-r--r-- | theories/Bool/Bvector.v | 5 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 5 | ||||
| -rw-r--r-- | theories/Program/Syntax.v | 2 |
3 files changed, 3 insertions, 9 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 7ecfa43f29..d9da086721 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -10,9 +10,8 @@ (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) -Require Export Bool. -Require Export Sumbool. -Require Import Arith. +Require Export Bool Sumbool. +Require Import Minus. Open Local Scope nat_scope. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 2456e1706d..b699b74287 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -8,10 +8,7 @@ (*i $Id$ i*) -Require Import Bool. -Require Import Bvector. -Require Import BinPos. -Require Import BinNat. +Require Import Bool Setoid Bvector BinPos BinNat. (** Operation over bits of a [N] number. *) 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]]. |