From 84d2679cd91758f02ff4cba41030b075ff0614df Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Tue, 28 Nov 2023 16:07:33 +1100 Subject: [PATCH] Correct some broken dependency-information (Including removal of unnecessary link to topologyTheory in fsgraph.) --- examples/Crypto/DES/Holmakefile | 2 +- examples/generic_finite_graphs/Holmakefile | 2 +- examples/generic_finite_graphs/fsgraphScript.sml | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/examples/Crypto/DES/Holmakefile b/examples/Crypto/DES/Holmakefile index 3964b30908..a7287fa6b3 100644 --- a/examples/Crypto/DES/Holmakefile +++ b/examples/Crypto/DES/Holmakefile @@ -1 +1 @@ -INCLUDES = $(HOLDIR)/src/n-bit +INCLUDES = $(HOLDIR)/src/n-bit $(HOLDIR)/src/res_quan/src diff --git a/examples/generic_finite_graphs/Holmakefile b/examples/generic_finite_graphs/Holmakefile index 34a91a8aa2..04378d56f1 100644 --- a/examples/generic_finite_graphs/Holmakefile +++ b/examples/generic_finite_graphs/Holmakefile @@ -1 +1 @@ -INCLUDES = $(HOLDIR)/src/finite_maps +INCLUDES = $(HOLDIR)/src/finite_maps $(HOLDIR)/src/transfer diff --git a/examples/generic_finite_graphs/fsgraphScript.sml b/examples/generic_finite_graphs/fsgraphScript.sml index dfd80c7f86..70b35193af 100644 --- a/examples/generic_finite_graphs/fsgraphScript.sml +++ b/examples/generic_finite_graphs/fsgraphScript.sml @@ -1,7 +1,7 @@ open HolKernel Parse boolLib bossLib; -open arithmeticTheory pairTheory listTheory pred_setTheory sortingTheory hurdUtils - topologyTheory; +open arithmeticTheory pairTheory listTheory pred_setTheory sortingTheory + hurdUtils open genericGraphTheory;