aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rwxr-xr-xtheories/Init/Prelude.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index e7ad28e3f..7325cc771 100755
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -9,8 +9,8 @@
(*i $Id$ i*)
Require Export Notations.
-Require Export Datatypes.
Require Export Logic.
+Require Export Datatypes.
Require Export Specif.
Require Export Peano.
Require Export Wf.