do not import Word in LittleEndian because it's defined purely on Z

mit-plv · Apr 5, 2024 · a392b79 · a392b79
1 parent 535508e
commit a392b79
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 5 deletions.
diff --git a/src/coqutil/Word/LittleEndian.v b/src/coqutil/Word/LittleEndian.v
@@ -1,7 +1,6 @@
 Require Import Coq.ZArith.ZArith.
 Require Import coqutil.Z.Lia.
-Require Import coqutil.Word.Interface coqutil.Datatypes.HList coqutil.Datatypes.PrimitivePair.
-Require Import coqutil.Word.Properties.
+Require Import coqutil.Datatypes.HList coqutil.Datatypes.PrimitivePair.
 Require Import coqutil.Z.bitblast.
 Require Import coqutil.Z.prove_Zeq_bitwise.
 Require Import coqutil.Byte.

diff --git a/src/coqutil/Word/LittleEndianList.v b/src/coqutil/Word/LittleEndianList.v
@@ -1,10 +1,9 @@
 Require Import Coq.ZArith.ZArith.
 Require Import coqutil.Z.Lia Coq.micromega.Lia.
-Require Import coqutil.Word.Interface.
-Require Import coqutil.Word.Properties.
 Require Import coqutil.Z.bitblast.
 Require Import coqutil.Z.prove_Zeq_bitwise.
 Require Import coqutil.Byte.
+Require Import coqutil.Z.PushPullMod.
 Require coqutil.Datatypes.List.
 
 Local Open Scope Z_scope.
@@ -160,7 +159,7 @@ Section LittleEndian.
     apply le_combine_inj.
     - rewrite !length_le_split; reflexivity.
     - rewrite !le_combine_split.
-      coqutil.Z.PushPullMod.Z.push_pull_mod; reflexivity.
+      Z.push_pull_mod; reflexivity.
   Qed.
 
   Lemma split_le_combine' bs n: