From 23cf55c1e2e5afb64eb1c45360fea840a12582d1 Mon Sep 17 00:00:00 2001 From: Heiko Becker <hbecker@mpi-sws.org> Date: Wed, 25 Mar 2020 08:18:47 +0100 Subject: [PATCH] Fix regression test for new infrastructure --- testcases/regression/Holmakefile | 2 +- testcases/regression/certificate_AdditionSimpleScript.sml | 2 +- testcases/regression/certificate_DopplerScript.sml | 2 +- testcases/regression/certificate_HimmilbeauScript.sml | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/testcases/regression/Holmakefile b/testcases/regression/Holmakefile index 1c723956..6c6bfcf5 100644 --- a/testcases/regression/Holmakefile +++ b/testcases/regression/Holmakefile @@ -1,4 +1,4 @@ -INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../../hol4 ../../hol4/Infra ../../hol4/cakeml/misc +INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../../hol4 ../../hol4/Infra OPTIONS = QUIT_ON_FAILURE ifdef POLY diff --git a/testcases/regression/certificate_AdditionSimpleScript.sml b/testcases/regression/certificate_AdditionSimpleScript.sml index 8965ff7f..5e0d64ff 100644 --- a/testcases/regression/certificate_AdditionSimpleScript.sml +++ b/testcases/regression/certificate_AdditionSimpleScript.sml @@ -1,4 +1,4 @@ -open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory; +open FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory; open simpLib realTheory realLib RealArith; val _ = new_theory "certificate_AdditionSimple"; diff --git a/testcases/regression/certificate_DopplerScript.sml b/testcases/regression/certificate_DopplerScript.sml index ec687ff3..27f2e7b0 100644 --- a/testcases/regression/certificate_DopplerScript.sml +++ b/testcases/regression/certificate_DopplerScript.sml @@ -1,4 +1,4 @@ -open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory; +open FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory; open simpLib realTheory realLib RealArith; val _ = new_theory "certificate_Doppler"; diff --git a/testcases/regression/certificate_HimmilbeauScript.sml b/testcases/regression/certificate_HimmilbeauScript.sml index 37a235cc..1f005403 100644 --- a/testcases/regression/certificate_HimmilbeauScript.sml +++ b/testcases/regression/certificate_HimmilbeauScript.sml @@ -1,4 +1,4 @@ -open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory; +open FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory; open simpLib realTheory realLib RealArith; val _ = new_theory "certificate_Himmilbeau"; -- GitLab