diff options
| -rw-r--r-- | theories/Numbers/NumPrelude.v | 1 |
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. (* |
