diff --git a/_CoqProject b/_CoqProject
index 68772ab..e69c368 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,14 +1,14 @@
--R . DedekindReals
+-Q theories DedekindReals
 
 -arg -w -arg -deprecated-instance-without-locality
 
-Additive.v
-Archimedean.v
-Cauchy.v
-Completeness.v
-Cut.v
-DecOrder.v
-MinMax.v
-MiscLemmas.v
-Multiplication.v
-Order.v
+theories/Additive.v
+theories/Archimedean.v
+theories/Cauchy.v
+theories/Completeness.v
+theories/Cut.v
+theories/DecOrder.v
+theories/MinMax.v
+theories/MiscLemmas.v
+theories/Multiplication.v
+theories/Order.v
diff --git a/Additive.v b/theories/Additive.v
similarity index 98%
rename from Additive.v
rename to theories/Additive.v
index 9aeaf59..1a0f766 100644
--- a/Additive.v
+++ b/theories/Additive.v
@@ -1,10 +1,10 @@
 (** The additive structure of reals. *)
 
-Require Import Setoid Morphisms SetoidClass.
-Require Import MiscLemmas.
-Require Import QArith QOrderedType Qminmax Qabs.
-Require Import Cut.
-Require Import Archimedean.
+From Coq Require Import Setoid Morphisms SetoidClass.
+From DedekindReals Require Import MiscLemmas.
+From Coq Require Import QArith QOrderedType Qminmax Qabs.
+From DedekindReals Require Import Cut.
+From DedekindReals Require Import Archimedean.
 
 Local Open Scope Q_scope.
 
diff --git a/Archimedean.v b/theories/Archimedean.v
similarity index 97%
rename from Archimedean.v
rename to theories/Archimedean.v
index bff8ab1..b8e57f3 100644
--- a/Archimedean.v
+++ b/theories/Archimedean.v
@@ -7,9 +7,9 @@
    can find a straddling pair (u, l). In other words, this means we cna find arbitrarily
    good lower and upper rational approximations to x. *)
 
-Require Import QArith.
-Require Import MiscLemmas.
-Require Import Cut.
+From Coq Require Import QArith.
+From DedekindReals Require Import MiscLemmas.
+From DedekindReals Require Import Cut.
 
 Local Open Scope Q_scope.
 
diff --git a/Cauchy.v b/theories/Cauchy.v
similarity index 98%
rename from Cauchy.v
rename to theories/Cauchy.v
index 769ac04..d91d9c4 100644
--- a/Cauchy.v
+++ b/theories/Cauchy.v
@@ -1,11 +1,11 @@
 (** The inclusion of Cauchy reals into Dedekind reals,
     and the proof that Dedekind reals are Cauchy-complete. *)
 
-Require Import QArith.
-Require Import Qabs.
-Require Import Qpower.
-Require Import Cut.
-Require Import MiscLemmas.
+From Coq Require Import QArith.
+From Coq Require Import Qabs.
+From Coq Require Import Qpower.
+From DedekindReals Require Import Cut.
+From DedekindReals Require Import MiscLemmas.
 
 Definition CauchyQ (un : nat -> Q) : Set
   := forall eps:Q,
diff --git a/Completeness.v b/theories/Completeness.v
similarity index 98%
rename from Completeness.v
rename to theories/Completeness.v
index f2c4b81..d065902 100644
--- a/Completeness.v
+++ b/theories/Completeness.v
@@ -3,9 +3,9 @@
    get R back. 
 *)
 
-Require Import Morphisms.
-Require Import QArith.
-Require Import Cut Order.
+From Coq Require Import Morphisms.
+From Coq Require Import QArith.
+From DedekindReals Require Import Cut Order.
 
 Local Open Scope R_scope.
 
diff --git a/Cut.v b/theories/Cut.v
similarity index 98%
rename from Cut.v
rename to theories/Cut.v
index 86893ab..2be632d 100644
--- a/Cut.v
+++ b/theories/Cut.v
@@ -1,8 +1,8 @@
 (** The definition of Dedekind cuts. *)
 
-Require Import QArith QOrderedType.
-Require Import Morphisms SetoidClass.
-Require Import MiscLemmas.
+From Coq Require Import QArith QOrderedType.
+From Coq Require Import Morphisms SetoidClass.
+From DedekindReals Require Import MiscLemmas.
 
 (** In the definition below we use disjunction and existence where one might
     expect sums and disjoint sums, in particular in [lower_open], [upper_open],
diff --git a/DecOrder.v b/theories/DecOrder.v
similarity index 96%
rename from DecOrder.v
rename to theories/DecOrder.v
index 6ca6ac7..dcdb2e2 100644
--- a/DecOrder.v
+++ b/theories/DecOrder.v
@@ -12,15 +12,15 @@
     The series vn is convergent, because bounded by the convergent
     series 2^{-n}. *)
 
-Require Import Logic.ConstructiveEpsilon.
-Require Import QArith.
-Require Import Qabs.
-Require Import Qpower.
-Require Import Cut.
-Require Import Cauchy.
-Require Import Additive.
-Require Import MiscLemmas.
-Require Import Qminmax.
+From Coq Require Import ConstructiveEpsilon.
+From Coq Require Import QArith.
+From Coq Require Import Qabs.
+From Coq Require Import Qpower.
+From DedekindReals Require Import Cut.
+From DedekindReals Require Import Cauchy.
+From DedekindReals Require Import Additive.
+From DedekindReals Require Import MiscLemmas.
+From Coq Require Import Qminmax.
 
 Local Open Scope R_scope.
 
diff --git a/MinMax.v b/theories/MinMax.v
similarity index 97%
rename from MinMax.v
rename to theories/MinMax.v
index cf454b4..4ed39f1 100644
--- a/MinMax.v
+++ b/theories/MinMax.v
@@ -1,10 +1,10 @@
 (* The lattice structure of the reals. *)
 
-Require Import Setoid Morphisms.
-Require Import QArith.
-Require Import Qminmax.
+From Coq Require Import Setoid Morphisms.
+From Coq Require Import QArith.
+From Coq Require Import Qminmax.
 
-Require Import Cut MiscLemmas Additive Multiplication Order.
+From DedekindReals Require Import Cut MiscLemmas Additive Multiplication Order.
 
 Local Open Scope R_scope.
 
diff --git a/MiscLemmas.v b/theories/MiscLemmas.v
similarity index 100%
rename from MiscLemmas.v
rename to theories/MiscLemmas.v
diff --git a/Multiplication.v b/theories/Multiplication.v
similarity index 99%
rename from Multiplication.v
rename to theories/Multiplication.v
index 6c81e6d..ae6ae53 100644
--- a/Multiplication.v
+++ b/theories/Multiplication.v
@@ -1,10 +1,10 @@
 (** The multiplicative structure of reals. *)
 
-Require Import Setoid Morphisms SetoidClass.
-Require Import MiscLemmas.
-Require Import QArith QOrderedType Qminmax Qabs.
-Require Import Psatz.
-Require Import Cut Additive Archimedean.
+From Coq Require Import Setoid Morphisms SetoidClass.
+From DedekindReals Require Import MiscLemmas.
+From Coq Require Import QArith QOrderedType Qminmax Qabs.
+From Coq Require Import Psatz.
+From DedekindReals Require Import Cut Additive Archimedean.
 
 Local Open Scope Q_scope.
 
diff --git a/Order.v b/theories/Order.v
similarity index 96%
rename from Order.v
rename to theories/Order.v
index 6310588..c02f2fe 100644
--- a/Order.v
+++ b/theories/Order.v
@@ -1,10 +1,10 @@
 (* The order relations < and <=. *)
 
-Require Import Morphisms Setoid.
-Require Import QArith.
-Require Import Cut.
-Require Import Additive Multiplication.
-Require Import Archimedean.
+From Coq Require Import Morphisms Setoid.
+From Coq Require Import QArith.
+From DedekindReals Require Import Cut.
+From DedekindReals Require Import Additive Multiplication.
+From DedekindReals Require Import Archimedean.
 
 Local Open Scope R_scope.