From 2eb778033fe37fa26adaf41d48fc630ef66c9d1d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 10 Sep 2020 21:58:31 +0200
Subject: [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.
---
 Makefile.build | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'Makefile.build')

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  $<'
-- 
cgit v1.2.3