diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-31 23:20:21 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-01 00:53:09 +0200 |
| commit | 1532e4d57fce07e8a1cd6838853a4a31ea84e453 (patch) | |
| tree | a1c3e1f1ca8b5924f60e3756a1f81a6ae8764c7e /Makefile.common | |
| 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 'Makefile.common')
| -rw-r--r-- | Makefile.common | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index e7d092876..2244e6867 100644 --- a/Makefile.common +++ b/Makefile.common @@ -85,6 +85,7 @@ CHKSRCDIRS:= config lib checker ########################################################################### COQDEP:=bin/coqdep$(EXE) +COQDEPBOOT:=bin/coqdep_boot$(EXE) OCAMLLIBDEP:=bin/ocamllibdep$(EXE) COQMAKEFILE:=bin/coq_makefile$(EXE) GALLINA:=bin/gallina$(EXE) @@ -258,7 +259,7 @@ CSDPCERTCMO:=$(addprefix plugins/micromega/, \ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma -COQDEPCMO:=$(COQENVCMO) lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo +COQDEPCMO:=$(COQENVCMO) lib/minisys.cmo lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo COQDOCCMO:=lib/clib.cma $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) |