diff --git a/.github/workflows/ci_build.yml b/.github/workflows/ci_build.yml
index 6ce979eb..cec17568 100644
--- a/.github/workflows/ci_build.yml
+++ b/.github/workflows/ci_build.yml
@@ -33,6 +33,7 @@ jobs:
         with:
           ocaml-compiler: ${{ env.OCAML_VER }}
           dune-cache: true
+          cache-prefix: "v2"
       - name: install Menhir and Coq
         run: |
           opam update
diff --git a/.gitignore b/.gitignore
index 7073d776..b4845316 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,8 +1,8 @@
 _build
 
 # Ignore generated parser code
-driver/parser.ml
-driver/parser.mli
+**/parser.ml
+**/parser.mli
 theories/**/Parser.v
 
 # Remove Coq compiled code
@@ -14,5 +14,5 @@ theories/**/Parser.v
 *.vok
 *.vos
 .lia.cache
-makefile.coq*
+CoqMakefile.mk*
 *.~undo-tree~
diff --git a/theories/Frontend/ParserExtraction.v b/theories/Frontend/ParserExtraction.v
index 6300aa05..65a33a3b 100644
--- a/theories/Frontend/ParserExtraction.v
+++ b/theories/Frontend/ParserExtraction.v
@@ -8,5 +8,4 @@ Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlNatInt.
 Require Import ExtrOcamlNativeString.
 
-(* Meant to be run in this directory *)
-Extraction "../driver/parser.ml" Parser.prog.
+Extraction "parser.ml" Parser.prog.
diff --git a/theories/Makefile b/theories/Makefile
new file mode 100644
index 00000000..4d2e7b9b
--- /dev/null
+++ b/theories/Makefile
@@ -0,0 +1,55 @@
+empty :=
+space := $(empty) $(empty)
+
+MENHIR := menhir
+
+COQMAKEFILE := CoqMakefile.mk
+COQPROJECTFILE := _CoqProject
+PARSERBASE := parser.ml
+PARSERFILE := ../driver/$(PARSERBASE)
+PARSEREXTRACTIONDIR := Frontend
+PARSEREXTRACTIONCOQFILE := $(PARSEREXTRACTIONDIR)/ParserExtraction.v
+PARSEREXTRACTIONRESULTFILE := $(PARSEREXTRACTIONDIR)/$(PARSERBASE)
+COQPARSERFILE := $(patsubst %.vy,%.v,$(shell find ./ -name '*.vy'))
+COQFILES := $(sort $(shell find ./ -name '*.v') $(COQPARSERFILE))
+
+.PHONY: all
+all: $(COQMAKEFILE)
+	@+$(MAKE) -f "$(COQMAKEFILE)" all
+	@+$(MAKE) "$(PARSERFILE)"
+
+.PHONY: clean
+clean: $(COQMAKEFILE)
+	@+$(MAKE) -f "$(COQMAKEFILE)" cleanall
+	@echo "CLEAN $(PARSERFILE) $(COQMAKEFILE) $(COQMAKEFILE).conf"
+	@rm -f "$(PARSERBASE)" "$(PARSERFILE)" "$(COQMAKEFILE)" "$(COQMAKEFILE).conf"
+
+.PHONY: update_CoqProject
+update_CoqProject: clean
+	(echo "-R . Mcltt"; \
+        echo ""; \
+        echo "-arg -w -arg -notation-overridden"; \
+        echo ""; \
+        echo -e "$(subst $(space),\n,$(COQFILES))") > "$(COQPROJECTFILE)"
+
+.PHONY: force
+force: ;
+
+$(COQMAKEFILE): $(COQPROJECTFILE)
+	$(COQBIN)coq_makefile -f "$(COQPROJECTFILE)" -o "$(COQMAKEFILE)"
+
+$(COQPARSERFILE): %.v : %.vy
+	$(MENHIR) --coq "$?"
+
+$(COQPROJECTFILE): ;
+
+$(PARSERBASE): $(PARSEREXTRACTIONCOQFILE)
+	@+$(MAKE) -f "$(COQMAKEFILE)" -B "$(patsubst %.v,%.vo,$?)"
+
+$(PARSERFILE): $(PARSEREXTRACTIONCOQFILE)
+	@+$(MAKE) -f "$(PARSERBASE)"
+	@echo "MOVE $(PARSERBASE) => $(PARSERFILE)"
+	@mv "$(PARSERBASE)" "$(PARSERFILE)"
+
+%: $(COQMAKEFILE) force
+	@+$(MAKE) -f "$(COQMAKEFILE)" "$@"
diff --git a/theories/makefile b/theories/makefile
deleted file mode 100644
index 746e4a73..00000000
--- a/theories/makefile
+++ /dev/null
@@ -1,29 +0,0 @@
-empty :=
-space := $(empty) $(empty)
-
-COQMAKEFILE := makefile.coq
-COQPARSERFILE := $(patsubst %.vy,%.v,$(shell find ./ -name '*.vy'))
-COQFILES := $(sort $(shell find ./ -name '*.v') $(COQPARSERFILE))
-
-.PHONY: all
-all: $(COQMAKEFILE)
-
--include $(COQMAKEFILE)
-
-clean::
-	rm -f $(COQMAKEFILE)
-	rm -f $(COQMAKEFILE).conf
-
-$(COQPARSERFILE): %.v : %.vy
-	menhir --coq "$?"
-
-$(COQMAKEFILE): _CoqProject
-	coq_makefile -f _CoqProject -o "$@"
-
-.PHONY: update_CoqProject
-update_CoqProject: cleanall
-	(echo "-R . Mcltt"; \
-        echo ""; \
-        echo "-arg -w -arg -notation-overridden"; \
-        echo ""; \
-        echo -e "$(subst $(space),\n,$(COQFILES))") > _CoqProject