diff --git a/adequacy.v b/theories/adequacy.v
similarity index 100%
rename from adequacy.v
rename to theories/adequacy.v
diff --git a/derived.v b/theories/derived.v
similarity index 100%
rename from derived.v
rename to theories/derived.v
diff --git a/heap.v b/theories/heap.v
similarity index 100%
rename from heap.v
rename to theories/heap.v
diff --git a/lang.v b/theories/lang.v
similarity index 100%
rename from lang.v
rename to theories/lang.v
diff --git a/lifetime.v b/theories/lifetime.v
similarity index 100%
rename from lifetime.v
rename to theories/lifetime.v
diff --git a/lifting.v b/theories/lifting.v
similarity index 100%
rename from lifting.v
rename to theories/lifting.v
diff --git a/memcpy.v b/theories/memcpy.v
similarity index 100%
rename from memcpy.v
rename to theories/memcpy.v
diff --git a/notation.v b/theories/notation.v
similarity index 100%
rename from notation.v
rename to theories/notation.v
diff --git a/perm.v b/theories/perm.v
similarity index 100%
rename from perm.v
rename to theories/perm.v
diff --git a/perm_incl.v b/theories/perm_incl.v
similarity index 100%
rename from perm_incl.v
rename to theories/perm_incl.v
diff --git a/proofmode.v b/theories/proofmode.v
similarity index 100%
rename from proofmode.v
rename to theories/proofmode.v
diff --git a/races.v b/theories/races.v
similarity index 100%
rename from races.v
rename to theories/races.v
diff --git a/tactics.v b/theories/tactics.v
similarity index 100%
rename from tactics.v
rename to theories/tactics.v
diff --git a/type.v b/theories/type.v
similarity index 100%
rename from type.v
rename to theories/type.v
diff --git a/type_incl.v b/theories/type_incl.v
similarity index 100%
rename from type_incl.v
rename to theories/type_incl.v
diff --git a/typing.v b/theories/typing.v
similarity index 100%
rename from typing.v
rename to theories/typing.v
diff --git a/wp_tactics.v b/theories/wp_tactics.v
similarity index 100%
rename from wp_tactics.v
rename to theories/wp_tactics.v