uds-psl · haansn08 · Jun 30, 2022 · Jun 30, 2022 · Aug 15, 2022 · Aug 17, 2022
diff --git a/.gitignore b/.gitignore
@@ -7,6 +7,8 @@
 // Coq Files
 CoqMakefile.conf
 *.vo
+*.vok
+*.vos
 *.glob
 *.aux
 *.d

diff --git a/.gitmodules b/.gitmodules
@@ -3,4 +3,7 @@
 	url = https://github.com/tebbi/coqdocjs.git
 [submodule "external/smpl"]
 	path = external/smpl
-	url = https://github.com/sigurdschneider/smpl.git
+	url = https://github.com/uds-psl/smpl.git
+[submodule "external/base"]
+	path = external/base
+	url = https://github.com/haansn08/base-library.git
diff --git a/_CoqProject b/_CoqProject
@@ -1,9 +1,8 @@
--R external/base/ "Shared"
+-R external/base/ "PslBase"
 -R external/smpl/theories/ smpl
 -I external/smpl/src/
 -R theories/ "ProgrammingTuringMachines"
 
--install none
 COQDOCFLAGS = "--charset utf-8 --parse-comments --with-header ./website/header.html --with-footer ./website/footer.html --index indexpage --coqlib https://coq.inria.fr/distrib/V8.8.1/stdlib/"
 
 # Basics

diff --git a/external/base b/external/base
diff --git a/external/base/.gitignore b/external/base/.gitignore
diff --git a/external/base/Base.v b/external/base/Base.v
diff --git a/external/base/Bijection.v b/external/base/Bijection.v
-Original file line number
+Diff line change
@@ Expand Up / @@ -7,6 +7,8 @@ @@
     // Coq Files
     CoqMakefile.conf
     *.vo
+    *.vok
+    *.vos
     *.glob
     *.aux
     *.d
@@ Expand Down @@