aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.dev
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-07-31 14:24:11 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-08-29 17:39:41 +0200
commit028de158153de94adfcb9d1e995259d833968951 (patch)
tree0f02a6c03094971a3c095795e6a190618e470d45 /Makefile.dev
parentcc58638a8d33084c5c9f85ab4d536307da2d7929 (diff)
[general] Merge parsing with highparsing, put toplevel at the top of the linking chain.
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