From 8446c9e32de1964044237e6aef3d68ed1812df59 Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Thu, 30 Jan 2025 23:51:07 -0500 Subject: [PATCH] remove some unneeded requires and imports --- bedrock2/src/bedrock2/MetricLeakageSemantics.v | 2 -- bedrock2/src/bedrock2/SemanticsRelations.v | 7 +------ 2 files changed, 1 insertion(+), 8 deletions(-) diff --git a/bedrock2/src/bedrock2/MetricLeakageSemantics.v b/bedrock2/src/bedrock2/MetricLeakageSemantics.v index abe1aeb7b..420aa9848 100644 --- a/bedrock2/src/bedrock2/MetricLeakageSemantics.v +++ b/bedrock2/src/bedrock2/MetricLeakageSemantics.v @@ -6,10 +6,8 @@ Require Import coqutil.Z.Lia. Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord. Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth. Require Export bedrock2.Memory. -Require Import Coq.Lists.List. Require Import bedrock2.MetricLogging. Require Import bedrock2.MetricCosts. -Require Import bedrock2.MetricSemantics. Require Import bedrock2.Semantics. Require Import bedrock2.LeakageSemantics. Require Import Coq.Lists.List. diff --git a/bedrock2/src/bedrock2/SemanticsRelations.v b/bedrock2/src/bedrock2/SemanticsRelations.v index 94c790069..6f923beed 100644 --- a/bedrock2/src/bedrock2/SemanticsRelations.v +++ b/bedrock2/src/bedrock2/SemanticsRelations.v @@ -1,19 +1,14 @@ Require Import coqutil.sanity coqutil.Byte. Require Import coqutil.Tactics.fwd. -Require Import coqutil.Map.Properties. -Require coqutil.Map.SortedListString. Require Import coqutil.Z.Lia. Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord. Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth. Require Export bedrock2.Memory. -Require Import Coq.Lists.List. Require Import bedrock2.MetricLogging. -Require Import bedrock2.MetricCosts. -Require Import bedrock2.MetricSemantics. Require Import bedrock2.Semantics. Require Import bedrock2.LeakageSemantics. +Require Import bedrock2.MetricSemantics. Require Import bedrock2.MetricLeakageSemantics. -Require Import Coq.Lists.List. Section MetricLeakageToSomething. Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word byte}.