From 6d8fa47f205e24a94416279fab41f09db6f02b8b Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 19 Jan 2021 02:44:03 +0000
Subject: Forgot to update ROOT

---
 ROOT | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ROOT b/ROOT
index b3aa520..014767a 100644
--- a/ROOT
+++ b/ROOT
@@ -29,4 +29,4 @@ session HoTT in hott = Spartan +
     Identity
     Equivalence
     Nat
-    "List+"
+    List_HoTT
-- 
cgit v1.2.3