aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2021-01-19 02:44:03 +0000
committerJosh Chen2021-01-19 02:44:03 +0000
commit6d8fa47f205e24a94416279fab41f09db6f02b8b (patch)
tree88749f620fc844cfea8801ef883b3b9cc1bd9660
parent549f1d46884d068ebf18f76bb359624510b086b0 (diff)
Forgot to update ROOT
-rw-r--r--ROOT2
1 files changed, 1 insertions, 1 deletions
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