diff --git a/export/export_common.sh b/export/export_common.sh
index 9ec89d6811cc10ca51f238450ca6e554e07d98b6..1e550cf588858de5f0b996f93e6399ace2bf8bab 100644
--- a/export/export_common.sh
+++ b/export/export_common.sh
@@ -25,7 +25,7 @@ ARCHIVE=`pwd`/$TARGET
 LOCAL=`pwd`
 
 # The absolute name of the root folder.
-SOURCES=`pwd`/../..
+SOURCES=`pwd`/../../theories
 
 # Wipe out a previous archive.
 rm -rf $ARCHIVE $ARCHIVE.tar.gz
diff --git a/Makefile.iris b/extra/Makefile.iris
similarity index 100%
rename from Makefile.iris
rename to extra/Makefile.iris
diff --git a/Makefile.model b/extra/Makefile.model
similarity index 100%
rename from Makefile.model
rename to extra/Makefile.model
diff --git a/Makefile.root b/extra/Makefile.root
similarity index 100%
rename from Makefile.root
rename to extra/Makefile.root
diff --git a/Example.v b/theories/Example.v
similarity index 100%
rename from Example.v
rename to theories/Example.v
diff --git a/ExampleBasic.v b/theories/ExampleBasic.v
similarity index 100%
rename from ExampleBasic.v
rename to theories/ExampleBasic.v
diff --git a/ExampleBasicNonlifted.v b/theories/ExampleBasicNonlifted.v
similarity index 100%
rename from ExampleBasicNonlifted.v
rename to theories/ExampleBasicNonlifted.v
diff --git a/ExampleHigherOrder.v b/theories/ExampleHigherOrder.v
similarity index 100%
rename from ExampleHigherOrder.v
rename to theories/ExampleHigherOrder.v
diff --git a/ExampleList.v b/theories/ExampleList.v
similarity index 100%
rename from ExampleList.v
rename to theories/ExampleList.v
diff --git a/ExampleListMosel.v b/theories/ExampleListMosel.v
similarity index 100%
rename from ExampleListMosel.v
rename to theories/ExampleListMosel.v
diff --git a/ExampleListNonlifted.v b/theories/ExampleListNonlifted.v
similarity index 100%
rename from ExampleListNonlifted.v
rename to theories/ExampleListNonlifted.v
diff --git a/ExampleQueueNonlifted.v b/theories/ExampleQueueNonlifted.v
similarity index 100%
rename from ExampleQueueNonlifted.v
rename to theories/ExampleQueueNonlifted.v
diff --git a/ExampleRO.v b/theories/ExampleRO.v
similarity index 100%
rename from ExampleRO.v
rename to theories/ExampleRO.v
diff --git a/ExampleROMosel.v b/theories/ExampleROMosel.v
similarity index 100%
rename from ExampleROMosel.v
rename to theories/ExampleROMosel.v
diff --git a/ExampleTrees.v b/theories/ExampleTrees.v
similarity index 100%
rename from ExampleTrees.v
rename to theories/ExampleTrees.v
diff --git a/ExampleUnionFind.v b/theories/ExampleUnionFind.v
similarity index 100%
rename from ExampleUnionFind.v
rename to theories/ExampleUnionFind.v
diff --git a/Fmap.v b/theories/Fmap.v
similarity index 100%
rename from Fmap.v
rename to theories/Fmap.v
diff --git a/LambdaCF.v b/theories/LambdaCF.v
similarity index 100%
rename from LambdaCF.v
rename to theories/LambdaCF.v
diff --git a/LambdaCFCredits.v b/theories/LambdaCFCredits.v
similarity index 100%
rename from LambdaCFCredits.v
rename to theories/LambdaCFCredits.v
diff --git a/LambdaCFLifted.v b/theories/LambdaCFLifted.v
similarity index 100%
rename from LambdaCFLifted.v
rename to theories/LambdaCFLifted.v
diff --git a/LambdaCFTactics.v b/theories/LambdaCFTactics.v
similarity index 100%
rename from LambdaCFTactics.v
rename to theories/LambdaCFTactics.v
diff --git a/LambdaSemantics.v b/theories/LambdaSemantics.v
similarity index 100%
rename from LambdaSemantics.v
rename to theories/LambdaSemantics.v
diff --git a/LambdaSep.v b/theories/LambdaSep.v
similarity index 100%
rename from LambdaSep.v
rename to theories/LambdaSep.v
diff --git a/LambdaSepCredits.v b/theories/LambdaSepCredits.v
similarity index 100%
rename from LambdaSepCredits.v
rename to theories/LambdaSepCredits.v
diff --git a/LambdaSepLifted.v b/theories/LambdaSepLifted.v
similarity index 100%
rename from LambdaSepLifted.v
rename to theories/LambdaSepLifted.v
diff --git a/LambdaSepMosel.v b/theories/LambdaSepMosel.v
similarity index 100%
rename from LambdaSepMosel.v
rename to theories/LambdaSepMosel.v
diff --git a/LambdaSepRO.v b/theories/LambdaSepRO.v
similarity index 100%
rename from LambdaSepRO.v
rename to theories/LambdaSepRO.v
diff --git a/LambdaSepROMosel.v b/theories/LambdaSepROMosel.v
similarity index 100%
rename from LambdaSepROMosel.v
rename to theories/LambdaSepROMosel.v
diff --git a/LambdaStruct.v b/theories/LambdaStruct.v
similarity index 100%
rename from LambdaStruct.v
rename to theories/LambdaStruct.v
diff --git a/LambdaStructLifted.v b/theories/LambdaStructLifted.v
similarity index 100%
rename from LambdaStructLifted.v
rename to theories/LambdaStructLifted.v
diff --git a/LambdaWP.v b/theories/LambdaWP.v
similarity index 100%
rename from LambdaWP.v
rename to theories/LambdaWP.v
diff --git a/LambdaWPLifted.v b/theories/LambdaWPLifted.v
similarity index 100%
rename from LambdaWPLifted.v
rename to theories/LambdaWPLifted.v
diff --git a/Makefile b/theories/Makefile
similarity index 100%
rename from Makefile
rename to theories/Makefile
diff --git a/SLHimpl.v b/theories/SLHimpl.v
similarity index 100%
rename from SLHimpl.v
rename to theories/SLHimpl.v
diff --git a/SLHprop.v b/theories/SLHprop.v
similarity index 100%
rename from SLHprop.v
rename to theories/SLHprop.v
diff --git a/SLRules.v b/theories/SLRules.v
similarity index 100%
rename from SLRules.v
rename to theories/SLRules.v
diff --git a/SLSemantics.v b/theories/SLSemantics.v
similarity index 100%
rename from SLSemantics.v
rename to theories/SLSemantics.v
diff --git a/SLWP.v b/theories/SLWP.v
similarity index 100%
rename from SLWP.v
rename to theories/SLWP.v
diff --git a/SepFunctor.v b/theories/SepFunctor.v
similarity index 100%
rename from SepFunctor.v
rename to theories/SepFunctor.v
diff --git a/SepMosel.v b/theories/SepMosel.v
similarity index 100%
rename from SepMosel.v
rename to theories/SepMosel.v
diff --git a/TLCbuffer.v b/theories/TLCbuffer.v
similarity index 100%
rename from TLCbuffer.v
rename to theories/TLCbuffer.v