diff options
| author | Emilio Jesus Gallego Arias | 2020-09-10 21:58:31 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-09-17 15:27:48 +0200 |
| commit | 2eb778033fe37fa26adaf41d48fc630ef66c9d1d (patch) | |
| tree | e28252dc8d989e9e5c43b87e2e37044372a35661 /Makefile.build | |
| parent | 14f0e5059e7f49cabbcd1571d7f053db7d7d3f35 (diff) | |
[build] Don't link `num` anymore in Coq
After #8743 we don't depend on `num` anymore in the codebase; thus we
drop the dependency.
This could create problems for plugins relying on this implicit
linking.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Makefile.build b/Makefile.build index 061489f47f..eed3c2813a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -302,7 +302,7 @@ $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^ endef # Main packages linked by Coq. -SYSMOD:=-package str,unix,dynlink,threads,num,zarith +SYSMOD:=-package str,unix,dynlink,threads,zarith ########################################################################### # Infrastructure for the rest of the Makefile @@ -587,11 +587,11 @@ CSDPCERTCMO:=clib/clib.cma $(addprefix plugins/micromega/, \ $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml, -package num,unix) + $(HIDE)$(call bestocaml, -package unix) $(CSDPCERTBYTE): $(CSDPCERTCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(call ocamlbyte, -package num,unix) + $(HIDE)$(call ocamlbyte, -package unix) ########################################################################### # tests @@ -707,7 +707,7 @@ COND_OPTFLAGS= \ plugins/micromega/%.cmi: plugins/micromega/%.mli $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix -c $< %.cmi: %.mli $(SHOW)'OCAMLC $<' @@ -715,7 +715,7 @@ plugins/micromega/%.cmi: plugins/micromega/%.mli plugins/micromega/%.cmo: plugins/micromega/%.ml $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< + $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix -c $< %.cmo: %.ml $(SHOW)'OCAMLC $<' @@ -752,7 +752,7 @@ plugins/micromega/csdpcert_FORPACK:= plugins/micromega/%.cmx: plugins/micromega/%.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $< + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix -c $< plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLOPT $<' |