aboutsummaryrefslogtreecommitdiff
path: root/checker/check.mllib
diff options
context:
space:
mode:
authorPierre Letouzey2016-05-31 23:20:21 +0200
committerPierre Letouzey2016-06-01 00:53:09 +0200
commit1532e4d57fce07e8a1cd6838853a4a31ea84e453 (patch)
treea1c3e1f1ca8b5924f60e3756a1f81a6ae8764c7e /checker/check.mllib
parentb3485ddc8c4f98743426bb58c8d49b76edd43d61 (diff)
Makefile: restore the use of coqdep_boot for creating .v.d files
Coqdep_boot has almost no dependencies, and hence can be compiled very early during the build, without relying on .ml.d files. Some code of system.ml is now in a separate file minisys.ml, which is also included in system.ml for compatibility.
Diffstat (limited to 'checker/check.mllib')
-rw-r--r--checker/check.mllib1
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/check.mllib b/checker/check.mllib
index 900cfe0c82..49de5e87f5 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -37,6 +37,7 @@ CEphemeron
Future
CUnix
+Minisys
System
Profile
RemoteCounter