aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/ZArith.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-28 23:30:32 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-28 23:30:32 +0000
commite97cd3c0cab1eb022b15d65bb33483055ce4cc28 (patch)
treee1fb56c8f3d5d83f68d55e6abdbb3486d137f9e2 /theories/ZArith/ZArith.v
parent00353bc0b970605ae092af594417a51a0cdf903f (diff)
Deletion of useless Zdigits_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14247 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/ZArith.v')
-rw-r--r--theories/ZArith/ZArith.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index abd735de5..265e62f06 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -12,7 +12,7 @@ Require Export ZArith_base.
(** Extra definitions *)
-Require Export Zpow_def Zdigits_def.
+Require Export Zpow_def.
(** Extra modules using [Omega] or [Ring]. *)