diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2013-12-16 17:08:46 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2013-12-16 17:24:55 +0100 |
| commit | 4759f60b04a278ecd46c8a120340ba55b185c6d1 (patch) | |
| tree | f5e24b08d23bd5efc9d0f80b86cde32ad548220f /Makefile.common | |
| parent | 9f005304183ca9c46f6516c08c3c0cc2f1efc05f (diff) | |
A few fixes to the build system (mostly for ocamlbuild)
* vars.mli was mentionning Term instead of Constr, leading to a dep cycle
* Having a file named toplevel/toplevel.ml isn't a good idea when we also
have a toplevel/toplevel.mllib that ought to produce a toplevel.cma.
We rename toplevel.ml into Coqloop.ml
* Extra cleanup of toplevel.mllib :
- Ppextra isn't anywhere around (?!)
- Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway
- Vernacexpr is a .mli and shouldn't appear in an .mllib
* During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml)
* A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread
for coqchk).
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index b13e828c4..d41fc909d 100644 --- a/Makefile.common +++ b/Makefile.common @@ -156,7 +156,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ - printing/printing.cma parsing/parsing.cma tactics/tactics.cma \ + parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma |