Reorganize theory structure. In particular, the identity type moves out from under Spartan to HoTT. Spartan now only has Pi and Sigma.

1 files changed, 14 insertions, 4 deletions

diff --git a/ROOT b/ROOT
index 09e3042..1e8017c 100644
--- a/ROOT
+++ b/ROOT
@@ -1,15 +1,23 @@
-session Spartan in "spartan/theories" = Pure +
+session Spartan_Core in "spartan/core" = Pure +
   description "
     Spartan type theory: a minimal dependent type theory based on
     intensional Martin-Löf type theory with cumulative Russell-style universes,
-    Pi, Sigma and identity types.
+    Pi, Sigma and identity types. This session consists only of the very core
+    theory files.
   "
   sessions
     "HOL-Eisbach"
   theories
     Spartan (global)
-    Identity
-    Equivalence
+
+session Spartan in spartan = Spartan_Core +
+  description "
+    Type theory based on Spartan, but with a few more bells and whistles.
+  "
+  directories
+    data
+  theories
+    "data/List"
 
 session HoTT in hott = Spartan +
   description "
@@ -21,5 +29,7 @@ session HoTT in hott = Spartan +
   "
   theories
     Base
+    Identity
+    Equivalence
     Nat