diff options
| author | Pierre Letouzey | 2016-05-31 23:20:21 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-06-01 00:53:09 +0200 |
| commit | 1532e4d57fce07e8a1cd6838853a4a31ea84e453 (patch) | |
| tree | a1c3e1f1ca8b5924f60e3756a1f81a6ae8764c7e /lib/lib.mllib | |
| parent | b3485ddc8c4f98743426bb58c8d49b76edd43d61 (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 'lib/lib.mllib')
| -rw-r--r-- | lib/lib.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/lib.mllib b/lib/lib.mllib index 2be435f6ff..a6c09058dd 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -3,6 +3,7 @@ Bigint Segmenttree Unicodetable Unicode +Minisys System CThread Spawn |