From 2feb56660700af107abb5a28a7120052ac405518 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 31 Jan 2021 02:54:51 +0000
Subject: rename things + some small changes

---
 ROOT | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'ROOT')

diff --git a/ROOT b/ROOT
index 014767a..2d97bbb 100644
--- a/ROOT
+++ b/ROOT
@@ -1,16 +1,16 @@
-session Spartan_Core in "spartan/core" = Pure +
+session MLTT_Core in "mltt/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 types and
-    Sigma types."
+    "Core MLTT: minimal dependent type theory based on intensional Martin-Löf
+    type theory with cumulative Russell-style universes, Pi types and Sigma
+    types."
   sessions
     "HOL-Eisbach"
   theories
-    Spartan (global)
+    MLTT (global)
 
-session Spartan in spartan = Spartan_Core +
+session MLTT in mltt = MLTT_Core +
   description
-    "Dependent type theory based on Spartan."
+    "Dependent type theory based on MLTT_Core."
   directories
     lib
   theories
@@ -18,7 +18,7 @@ session Spartan in spartan = Spartan_Core +
     Maybe
     List
 
-session HoTT in hott = Spartan +
+session HoTT in hott = MLTT +
   description
     "Homotopy type theory, following the development in
       The Univalent Foundations Program,
-- 
cgit v1.2.3