remove some unneeded requires and imports

mit-plv · Jan 31, 2025 · 8446c9e · 8446c9e
1 parent e151241
commit 8446c9e
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 8 deletions.
diff --git 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
@@ -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}.