From 8eccaf28cdf482a8640c2a7b910c9d42de55e596 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 5 Dec 2024 14:16:12 +0100
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530 (#1992)

---
 src/Bedrock/End2End/RupicolaCrypto/Broadcast.v | 4 +++-
 src/Bedrock/End2End/RupicolaCrypto/Spec.v      | 4 +++-
 2 files changed, 6 insertions(+), 2 deletions(-)

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.