From 2e268b6ba5e6f5e0ba87a09f4cf90d2ac0dc06b8 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 12 Dec 2022 17:29:33 -0500 Subject: [PATCH] saw-core-coq: Delete duplicate sawCoreScaffoldingModule definition The `SpecialTreatment` module had two entirely duplicate definitions (`sawCoreScaffoldingModule` and `sawDefinitionsModule`) referring to the `SAWCoreScaffolding` module. Let's delete the former in favor of the latter, which is more widely used. --- .../src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs index c4c763a874..717df91833 100644 --- a/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs +++ b/saw-core-coq/src/Verifier/SAW/Translation/Coq/SpecialTreatment.hs @@ -211,9 +211,6 @@ sawVectorDefinitionsModule (TranslationConfiguration {..}) = cryptolPrimitivesModule :: ModuleName cryptolPrimitivesModule = mkModuleName ["CryptolPrimitivesForSAWCore"] -sawCoreScaffoldingModule :: ModuleName -sawCoreScaffoldingModule = mkModuleName ["SAWCoreScaffolding"] - preludeExtraModule :: ModuleName preludeExtraModule = mkModuleName ["SAWCorePreludeExtra"] @@ -246,7 +243,7 @@ sawCorePreludeSpecialTreatmentMap configuration = Map.fromList $ -- sawLet - [ ("sawLet", mapsTo sawCoreScaffoldingModule "sawLet_def") ] + [ ("sawLet", mapsTo sawDefinitionsModule "sawLet_def") ] -- Unsafe SAW features ++ @@ -363,8 +360,8 @@ sawCorePreludeSpecialTreatmentMap configuration = [ ("divModNat", mapsTo sawDefinitionsModule "divModNat") , ("Nat", mapsTo datatypesModule "nat") , ("widthNat", mapsTo sawDefinitionsModule "widthNat") - , ("Zero", mapsTo sawCoreScaffoldingModule "Zero") - , ("Succ", mapsTo sawCoreScaffoldingModule "Succ") + , ("Zero", mapsTo sawDefinitionsModule "Zero") + , ("Succ", mapsTo sawDefinitionsModule "Succ") ] -- Vectors