From ff8bfa4e4a1a76c1f431b45c1b644ae9249b8170 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 26 Apr 2021 08:58:43 -0400 Subject: [PATCH] Fix generation of library dep graphs Since we are not passing all .v files, we cannot use `-f _CoqProject` to invoke coqdep. Since we are not using `-f _CoqProject`, we must pass all of the `COQLIBS` arguments, not just the ones that got passed on the command line. --- Makefile.coq.local | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile.coq.local b/Makefile.coq.local index 8f0fef29fd0..04528c4b01c 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -135,11 +135,11 @@ strict: strict-test strict-no-axiom hottlib hott-core hott-categories contrib # The deps file, for graphs HoTT.deps: $(ALL_VFILES) $(SHOW)'COQDEP > $@' - $(HIDE)$(COQDEP) $(CMDLINE_COQLIBS) $(ALL_VFILES) | sed s'#\\#/#g' >$@ + $(HIDE)$(COQDEP) $(COQLIBS) $(ALL_VFILES) | sed s'#\\#/#g' >$@ HoTTCore.deps: $(CORE_VFILES) $(SHOW)'COQDEP > $@' - $(HIDE)$(COQDEP) $(CMDLINE_COQLIBS) $(CORE_VFILES) | sed s'#\\#/#g' >$@ + $(HIDE)$(COQDEP) $(COQLIBS) $(CORE_VFILES) | sed s'#\\#/#g' >$@ # The HTML files # We have a dummy file, to allow us to depend on the html files