aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--theories/Numbers/NumPrelude.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 05e9051708..904145d503 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -11,7 +11,6 @@
(*i $Id$ i*)
Require Export Setoid.
-Require Export QRewrite.
Set Implicit Arguments.
(*