summaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common15
1 files changed, 9 insertions, 6 deletions
diff --git a/Makefile.common b/Makefile.common
index 1889afc8..15faace0 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -66,8 +66,7 @@ COQTEX:=bin/coq-tex$(EXE)
COQWC:=bin/coqwc$(EXE)
COQDOC:=bin/coqdoc$(EXE)
-TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) \
- $(COQWC) $(COQDOC)
+TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC)
###########################################################################
# Documentation
@@ -404,11 +403,15 @@ CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx)
DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep.cmo
+COQDEPCMX:=$(COQDEPCMO:.cmo=.cmx)
+
GALLINACMO:=tools/gallina_lexer.cmo tools/gallina.cmo
+GALLINACMX:=$(GALLINACMO:.cmo=.cmx)
+
COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \
tools/coqdoc/index.cmo tools/coqdoc/output.cmo \
tools/coqdoc/pretty.cmo tools/coqdoc/main.cmo
-
+COQDOCCMX:=$(COQDOCCMO:.cmo=.cmx)
# checker
@@ -418,15 +421,15 @@ MCHECKER:=\
lib/flags.cmo lib/util.cmo lib/option.cmo lib/hashcons.cmo \
lib/system.cmo lib/envars.cmo \
lib/predicate.cmo lib/rtree.cmo \
- kernel/names.cmo kernel/univ.cmo \
- kernel/esubst.cmo checker/term.cmo \
+ kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo \
+ checker/validate.cmo \
+ checker/term.cmo \
checker/declarations.cmo checker/environ.cmo \
checker/closure.cmo checker/reduction.cmo \
checker/type_errors.cmo \
checker/modops.cmo \
checker/inductive.cmo checker/typeops.cmo \
checker/indtypes.cmo checker/subtyping.cmo checker/mod_checking.cmo \
- checker/validate.cmo \
checker/safe_typing.cmo checker/check.cmo \
checker/check_stat.cmo checker/checker.cmo