aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.dev
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-12-22 14:11:55 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-12-27 14:19:59 +0100
commitb37d3f199e4521e2ae20cc96f0f2b04acc36c7cc (patch)
tree5286af838087a280405b1cf1c7a3248612e7c5aa /Makefile.dev
parent7e319ad03aba413f3165b848eaf821b364f9291b (diff)
[API] remove large file containing duplicate interfaces
... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dev b/Makefile.dev
index d2a1e9235..db83be369 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -119,7 +119,7 @@ pretyping: pretyping/pretyping.cma
stm: stm/stm.cma
toplevel: toplevel/toplevel.cma
-.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping API
+.PHONY: lib kernel byterun library proofs tactics interp parsing pretyping
.PHONY: engine stm toplevel
######################