Adapt to coq/coq#19530 (#1992)

mit-plv · Dec 5, 2024 · 8eccaf2 · 8eccaf2
1 parent 6ab4d30
commit 8eccaf2
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git 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
@@ -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.