diff --git a/src/Bedrock/End2End/RupicolaCrypto/Broadcast.v b/src/Bedrock/End2End/RupicolaCrypto/Broadcast.v
index a8a84d3aa3..005405fc6d 100644
--- a/src/Bedrock/End2End/RupicolaCrypto/Broadcast.v
+++ b/src/Bedrock/End2End/RupicolaCrypto/Broadcast.v
@@ -2,7 +2,9 @@ From Coq Require Import Utf8.
 Require Import Rupicola.Lib.Api.
 Require Import Rupicola.Lib.Loops.
 
-From Coq Require Init.Byte String. Import Init.Byte(byte(..)) String.
+From Coq Require Init.Byte String.
+From Coq Require Import Init.Byte(byte(..)).
+Import String.
 Require Import coqutil.Datatypes.List. Import Lists.List List.ListNotations.
 From Coq Require Import BinInt. Import Zdiv. Local Open Scope Z_scope.
 Require Import coqutil.Byte coqutil.Word.LittleEndianList.
diff --git a/src/Bedrock/End2End/RupicolaCrypto/Spec.v b/src/Bedrock/End2End/RupicolaCrypto/Spec.v
index 2cf03c3334..30839cf4b4 100644
--- a/src/Bedrock/End2End/RupicolaCrypto/Spec.v
+++ b/src/Bedrock/End2End/RupicolaCrypto/Spec.v
@@ -1,4 +1,6 @@
-From Coq Require Init.Byte String. Export Init.Byte(byte(..)) String.
+From Coq Require Init.Byte String.
+From Coq Require Export Init.Byte(byte(..)).
+Export String.
 Require Export coqutil.Datatypes.List. Export Lists.List List.ListNotations.
 From Coq Require Export BinInt. Export Zdiv. Local Open Scope Z_scope.
 Require Export coqutil.Byte coqutil.Word.LittleEndianList.