diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-17 13:44:32 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-17 13:44:32 +0000 |
| commit | c710be6c4d2fda836939c404a1795e8a9171634e (patch) | |
| tree | f3e88e762686b03d7d3a98655a7e2f75db652846 /theories/NArith/Ndigits.v | |
| 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
Diffstat (limited to 'theories/NArith/Ndigits.v')
| -rw-r--r-- | theories/NArith/Ndigits.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 2456e1706..b699b7428 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. *) |