diff --git a/.gitmodules b/.gitmodules
@@ -2735,3 +2735,12 @@
 [submodule "2024/01/27/jscoq"]
 	path = 2024/01/27/jscoq
 	url = https://github.com/jscoq/jscoq
+[submodule "2024/01/27/coq-introspector-plugin"]
+	path = 2024/01/27/coq-introspector-plugin
+	url = https://github.com/meta-introspector/coq-introspector-plugin
+[submodule "2024/01/27/assistants"]
+	path = 2024/01/27/assistants
+	url = https://github.com/stellar-amenities/assistants
+[submodule "2024/01/27/coq-of-rust"]
+	path = 2024/01/27/coq-of-rust
+	url = https://github.com/formal-land/coq-of-rust
diff --git a/2023/07/06/Coq-Equations b/2023/07/06/Coq-Equations
diff --git a/2023/07/06/metacoq b/2023/07/06/metacoq
diff --git a/2023/07/12/coq-lsp b/2023/07/12/coq-lsp
diff --git a/2023/10/30/ollama b/2023/10/30/ollama
diff --git a/2023/12/28/coq-of-ocaml b/2023/12/28/coq-of-ocaml
diff --git a/2024/01/05/UniMath b/2024/01/05/UniMath
diff --git a/2024/01/07/ppx-introspector b/2024/01/07/ppx-introspector
diff --git a/2024/01/15/lang_agent b/2024/01/15/lang_agent
diff --git a/2024/01/27/assistants b/2024/01/27/assistants
diff --git a/2024/01/27/coq-introspector-plugin b/2024/01/27/coq-introspector-plugin
diff --git a/2024/01/27/coq-of-rust b/2024/01/27/coq-of-rust
+3 −3		.github/workflows/build.yml
+15 −0		.vscode/Coq-Equations.code-workspace
+6 −6		README.md
+2 −5		coq-equations.opam
+1 −1		doc/equations.tex
+2 −2		examples/HoTT_light.v
+5 −5		examples/MoreDep.v
+1 −1		examples/RoseTree.v
+2 −4		examples/STLC.v
+1 −1		examples/general_recursion.v
+2 −0		examples/string_matching.v
+1 −1		siteexamples.sh
+12 −12		src/context_map.ml
+4 −4		src/context_map.mli
+32 −29		src/covering.ml
+3 −3		src/covering.mli
+27 −24		src/depelim.ml
+3 −3		src/eqdec.ml
+17 −1		src/equations.ml
+3 −3		src/equations.mli
+50 −23		src/equations_common.ml
+9 −6		src/equations_common.mli
+1 −1		src/extra_tactics.ml
+8 −9		src/g_equations.mlg
+11 −11		src/noconf.ml
+9 −9		src/noconf_hom.ml
+39 −33		src/principles.ml
+228 −124		src/principles_proofs.ml
+14 −4		src/principles_proofs.mli
+36 −30		src/sigma_types.ml
+5 −5		src/sigma_types.mli
+30 −30		src/simplify.ml
+1 −1		src/simplify.mli
+32 −13		src/splitting.ml
+1 −1		src/splitting.mli
+23 −19		src/subterm.ml
+18 −20		src/syntax.ml
+4 −4		src/syntax.mli
+3 −2		test-suite/Basics.v
+7 −7		test-suite/BasicsHoTT.v
+2 −2		test-suite/DataStruct.v
+9 −8		test-suite/fin.v
+5 −4		test-suite/gcd.v
+1 −0		test-suite/issues/issue129.v
+1 −0		test-suite/issues/issue193.v
+1 −0		test-suite/issues/issue321.v
+4 −4		test-suite/issues/issue349.v
+2 −0		test-suite/issues/issue354.v
+1 −0		test-suite/issues/issue372.v
+1 −1		test-suite/issues/issue95_2.v
+1 −0		test-suite/local_where.v
+1 −0		test-suite/nestfixnorec.v
+8 −2		test-suite/rec.v
+1 −0		test-suite/rose.v
+2 −1		test-suite/zoe.v
+1 −1		theories/HoTT/DepElim.v