aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.dev
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev3
1 files changed, 1 insertions, 2 deletions
diff --git a/Makefile.dev b/Makefile.dev
index b0299bd16..dc4ded397 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -116,12 +116,11 @@ tactics: tactics/tactics.cma
interp: interp/interp.cma
parsing: parsing/parsing.cma
pretyping: pretyping/pretyping.cma
-highparsing: parsing/highparsing.cma
stm: stm/stm.cma
toplevel: toplevel/toplevel.cma
.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping API
-.PHONY: engine highparsing stm toplevel
+.PHONY: engine stm toplevel
######################
### 3) theories files