Removed equations, which was causing errors

addons/Makefile

-PKGS =  teach equations
+PKGS =  teach
 
 CONTEXT = jscoq+32bit
 ifeq ($(DUNE_WORKSPACE:%.64=64), 64)
@@ -46,7 +46,6 @@ endif
 
 world:
 	cd teach          && make
-	cd equations      && make
 
 privates:
 

addons/equations/.gitignore

-.*.swp
-/workdir
-_build

addons/equations/Makefile

-REPO = https://github.com/mattam82/Coq-Equations.git
-TAG = v1.3-8.17
-WORKDIR = workdir
-
-.PHONY: all get
-
-all: $(WORKDIR)
-	# not parallel: some Dune dependency mixup with generating META file
-	dune build -j1
-
-get: $(WORKDIR)
-
-$(WORKDIR):
-	git clone --depth=1 --no-checkout -b $(TAG) $(REPO) $(WORKDIR)
-	( cd $(WORKDIR) && git checkout $(TAG) && git apply ../patches/legacy-compat.patch )
-	rm $(WORKDIR)/theories/HoTT/dune  # HoTT still not available for 8.14
-

addons/equations/README.md

-# addon-equations
-Coq-Equations addon plugin for jsCoq

addons/equations/coq-equations.json

-{
-    "rootdir": "workdir",
-    "builddir": "coq-pkgs",
-    "projects": {
-        "equations": {
-            "theories": {
-                "prefix": "Equations"
-            },
-            "src": {
-                "prefix": "Equations"
-            }
-        }
-    }
-}

addons/equations/dune

-
-(rule
- (targets coq-pkgs)
- (deps
-  (package coq-equations)
-  workdir/src/equations_plugin.cma
-  (:pkg-json coq-equations.json))
- (action
-  (run npx %{env:pkgtool=jscoq} build %{pkg-json})))
-
-(alias
- (name all)
- (deps package.json))
-
-(dirs workdir)

addons/equations/package.json

-{
-    "name": "@jscoq/equations",
-    "description": "Equations 1.3 for jsCoq",
-    "version": "0.17.0",
-    "files": ["README.md", "coq-pkgs"],
-    "repository": {
-        "type": "git",
-        "url": "github:jscoq/addon-equations"
-    },
-    "license": "AGPL-3.0-or-later"
-}

addons/equations/patches/legacy-compat.patch

-diff --git a/theories/Type/Loader.v b/theories/Type/Loader.v
-index c3e7ed9..16cbcca 100644
---- a/theories/Type/Loader.v
-+++ b/theories/Type/Loader.v
-@@ -11,7 +11,7 @@
- Require Import Extraction.
- 
- (** This exports tactics *)
--Declare ML Module "coq-equations.plugin".
-+Declare ML Module "equations_plugin:coq-equations.plugin".
- 
- Set Warnings "-notation-overridden".
- From Equations Require Export Init Signature.
-@@ -32,4 +32,4 @@ Global Obligation Tactic := Equations.CoreTactics.equations_simpl.
- Ltac solve_rec := simpl in * ; cbv zeta ; intros ;
-   try typeclasses eauto with subterm_relation Below rec_decision.
- 
--Export EquationsNotations.
-\ No newline at end of file
-+Export EquationsNotations.