diff options
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/Makefile.common b/Makefile.common index 1a903539c2..86a7ea8476 100644 --- a/Makefile.common +++ b/Makefile.common @@ -63,7 +63,7 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) CORESRCDIRS:=\ config lib kernel kernel/byterun library \ proofs tactics pretyping interp stm \ - toplevel parsing printing grammar intf + toplevel parsing printing intf engine ltac PLUGINS:=\ omega romega micromega quote \ @@ -78,9 +78,7 @@ SRCDIRS:=\ IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils -# Order is relevant here because kernel and checker contain files -# with the same name -CHKSRCDIRS:= checker lib config kernel parsing +CHKSRCDIRS:= config lib checker ########################################################################### # Tools @@ -88,6 +86,7 @@ CHKSRCDIRS:= checker lib config kernel parsing COQDEP:=bin/coqdep$(EXE) COQDEPBOOT:=bin/coqdep_boot$(EXE) +OCAMLLIBDEP:=bin/ocamllibdep$(EXE) COQMAKEFILE:=bin/coq_makefile$(EXE) GALLINA:=bin/gallina$(EXE) COQTEX:=bin/coq-tex$(EXE) @@ -99,7 +98,7 @@ COQWORKMGR:=bin/coqworkmgr$(EXE) TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ $(COQWORKMGR) -PRIVATEBINARIES:=$(FAKEIDE) $(COQDEPBOOT) +PRIVATEBINARIES:=$(FAKEIDE) $(OCAMLLIBDEP) $(COQDEPBOOT) ########################################################################### # Documentation @@ -161,14 +160,14 @@ BYTERUN:=$(addprefix kernel/byterun/, \ coq_fix_code.o coq_memory.o coq_values.o coq_interp.o ) # LINK ORDER: -# Beware that highparsing.cma should appear before hightactics.cma +# Beware that highparsing.cma should appear before ltac.cma # respecting this order is useful for developers that want to load or link # the libraries directly CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ - pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ + engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ - stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma + stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma @@ -231,7 +230,7 @@ endif LINKCMO:=$(CORECMA) $(STATICPLUGINS) LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) -IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo +IDEDEPS:=lib/clib.cma lib/errors.cmo lib/spawn.cmo IDECMA:=ide/ide.cma IDETOPLOOPCMA=ide/coqidetop.cma @@ -260,7 +259,7 @@ CSDPCERTCMO:=$(addprefix plugins/micromega/, \ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma -COQDEPCMO:=$(COQENVCMO) 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 ) @@ -377,9 +376,9 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ OCAMLDOCDIR=dev/ocamldoc DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ - ./pretyping/*.mli ./interp/*.mli printing/*.mli \ + ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \ ./parsing/*.mli ./proofs/*.mli \ - ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli) + ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli) # Defining options to generate dependencies graphs DOT=dot |