From 0072da9d56061a2e4da179a3b9bb05452da10c06 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sun, 28 Jul 2024 10:35:40 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530

---
 etc/notes/poly1305_scratchpad.v                         | 2 +-
 src/Rupicola/Examples/Assoc/Assoc.v                     | 6 +++---
 src/Rupicola/Examples/CRC32/Table.v                     | 2 +-
 src/Rupicola/Examples/CapitalizeThird/CapitalizeThird.v | 6 +++---
 src/Rupicola/Examples/CapitalizeThird/Properties.v      | 8 ++++----
 src/Rupicola/Examples/IO/IO.v                           | 2 +-
 src/Rupicola/Examples/KVStore/kv.v                      | 2 +-
 src/Rupicola/Examples/RevComp.v                         | 4 ++--
 src/Rupicola/Examples/Swap/Properties.v                 | 6 +++---
 src/Rupicola/Examples/Swap/Swap.v                       | 6 +++---
 src/Rupicola/Examples/Uppercase.v                       | 4 ++--
 src/Rupicola/Lib/Core.v                                 | 2 +-
 src/Rupicola/Lib/Gensym.v                               | 3 +--
 src/Rupicola/Lib/IdentParsing.v                         | 4 ++--
 src/Rupicola/Lib/Monads.v                               | 2 +-
 src/Rupicola/Lib/ToCString.v                            | 4 ++--
 16 files changed, 31 insertions(+), 32 deletions(-)

diff --git a/etc/notes/poly1305_scratchpad.v b/etc/notes/poly1305_scratchpad.v
index 31214c83..12e429bb 100644
--- a/etc/notes/poly1305_scratchpad.v
+++ b/etc/notes/poly1305_scratchpad.v
@@ -2,7 +2,7 @@
 
 Require Coq.Init.Byte Coq.Strings.String. Import Init.Byte(byte(..)) String.
 Require Import coqutil.Datatypes.List. Import Lists.List List.ListNotations.
-Require Import Coq.ZArith.BinInt. Import Zdiv. Local Open Scope Z_scope.
+From Coq Require Import BinInt. Import Zdiv. Local Open Scope Z_scope.
 Require Import coqutil.Byte coqutil.Word.LittleEndianList.
 
 (* reference: https://datatracker.ietf.org/doc/html/rfc8439 *)
diff --git a/src/Rupicola/Examples/Assoc/Assoc.v b/src/Rupicola/Examples/Assoc/Assoc.v
index e850ce7e..0871fd25 100644
--- a/src/Rupicola/Examples/Assoc/Assoc.v
+++ b/src/Rupicola/Examples/Assoc/Assoc.v
@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import String.
+From Coq Require Import List.
 Require Import bedrock2.Syntax. Import Syntax.Coercions.
 Require Import bedrock2.NotationsCustomEntry.
 (* Require bedrock2.WeakestPrecondition. *)
diff --git a/src/Rupicola/Examples/CRC32/Table.v b/src/Rupicola/Examples/CRC32/Table.v
index f173a50d..edc28518 100644
--- a/src/Rupicola/Examples/CRC32/Table.v
+++ b/src/Rupicola/Examples/CRC32/Table.v
@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith Coq.Lists.List.
+From Coq Require Import ZArith List.
 Import ListNotations.
 Open Scope Z_scope.
 
diff --git a/src/Rupicola/Examples/CapitalizeThird/CapitalizeThird.v b/src/Rupicola/Examples/CapitalizeThird/CapitalizeThird.v
index 669c87da..10a538fc 100644
--- a/src/Rupicola/Examples/CapitalizeThird/CapitalizeThird.v
+++ b/src/Rupicola/Examples/CapitalizeThird/CapitalizeThird.v
@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import String.
+From Coq Require Import List.
 Require Import bedrock2.Syntax. Import Syntax.Coercions.
 Require Import bedrock2.NotationsCustomEntry.
 Require bedrock2.WeakestPrecondition.
diff --git a/src/Rupicola/Examples/CapitalizeThird/Properties.v b/src/Rupicola/Examples/CapitalizeThird/Properties.v
index 1fdab987..4332451f 100644
--- a/src/Rupicola/Examples/CapitalizeThird/Properties.v
+++ b/src/Rupicola/Examples/CapitalizeThird/Properties.v
@@ -1,7 +1,7 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
-Require Import Coq.micromega.Lia.
+From Coq Require Import ZArith.
+From Coq Require Import String.
+From Coq Require Import List.
+From Coq Require Import Lia.
 Require Import bedrock2.Array.
 Require Import bedrock2.NotationsCustomEntry.
 Require Import bedrock2.Scalars.
diff --git a/src/Rupicola/Examples/IO/IO.v b/src/Rupicola/Examples/IO/IO.v
index 37b5c888..19c3a9d0 100644
--- a/src/Rupicola/Examples/IO/IO.v
+++ b/src/Rupicola/Examples/IO/IO.v
@@ -1,4 +1,4 @@
-From Coq Require Logic.Eqdep Sets.Ensembles.
+From Coq Require Eqdep Ensembles.
 Require Import Rupicola.Lib.Api.
 Require Export Rupicola.Examples.IO.Writer.
 
diff --git a/src/Rupicola/Examples/KVStore/kv.v b/src/Rupicola/Examples/KVStore/kv.v
index 3ee0f482..c46cd855 100644
--- a/src/Rupicola/Examples/KVStore/kv.v
+++ b/src/Rupicola/Examples/KVStore/kv.v
@@ -158,7 +158,7 @@ Definition buf_unborrow_data (b: Buffer) (bs: Bytes) :=
 
 Require Import Arith PeanoNat.
 
-Require Import Coq.Program.Wf.
+From Coq.Program Require Import Wf.
 Require Import Psatz.
 
 Program Fixpoint ranged_for_nat {A}
diff --git a/src/Rupicola/Examples/RevComp.v b/src/Rupicola/Examples/RevComp.v
index b9f96793..7e8b4700 100644
--- a/src/Rupicola/Examples/RevComp.v
+++ b/src/Rupicola/Examples/RevComp.v
@@ -1,5 +1,5 @@
 (* https://benchmarksgame-team.pages.debian.net/benchmarksgame/description/revcomp.html *)
-Require Import Coq.Strings.String Coq.Strings.Ascii.
+From Coq Require Import String Ascii.
 
 Section Spec.
   Open Scope string_scope.
@@ -37,7 +37,7 @@ Section Spec.
   Compute revcomp_spec "RUPICOLA".
 End Spec.
 
-Require Import Coq.Strings.Byte.
+From Coq Require Import Strings.Byte.
 Require Import Rupicola.Lib.Api.
 Require Import Rupicola.Lib.Loops.
 Require Import Rupicola.Lib.Arrays.
diff --git a/src/Rupicola/Examples/Swap/Properties.v b/src/Rupicola/Examples/Swap/Properties.v
index 37c51adc..bcd527c5 100644
--- a/src/Rupicola/Examples/Swap/Properties.v
+++ b/src/Rupicola/Examples/Swap/Properties.v
@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import String.
+From Coq Require Import List.
 Require Import bedrock2.BasicC64Semantics.
 Require Import bedrock2.NotationsCustomEntry.
 Require Import bedrock2.ProgramLogic.
diff --git a/src/Rupicola/Examples/Swap/Swap.v b/src/Rupicola/Examples/Swap/Swap.v
index 4e091adc..f13fb6db 100644
--- a/src/Rupicola/Examples/Swap/Swap.v
+++ b/src/Rupicola/Examples/Swap/Swap.v
@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import String.
+From Coq Require Import List.
 Require Import bedrock2.Syntax. Import Syntax.Coercions.
 Require Import bedrock2.NotationsCustomEntry.
 Require bedrock2.WeakestPrecondition.
diff --git a/src/Rupicola/Examples/Uppercase.v b/src/Rupicola/Examples/Uppercase.v
index 768dc7b2..b1c8e1c1 100644
--- a/src/Rupicola/Examples/Uppercase.v
+++ b/src/Rupicola/Examples/Uppercase.v
@@ -1,4 +1,4 @@
-Require Import Coq.Strings.String Coq.Strings.Ascii.
+From Coq Require Import String Ascii.
 
 Section Spec.
   Open Scope string_scope.
@@ -26,7 +26,7 @@ Section Spec.
   Compute upstr_spec "rupicola".
 End Spec.
 
-Require Import Coq.Strings.Byte.
+From Coq Require Import Strings.Byte.
 Require Import Rupicola.Lib.Api.
 Require Import Rupicola.Lib.Loops.
 Require Import Rupicola.Lib.Arrays.
diff --git a/src/Rupicola/Lib/Core.v b/src/Rupicola/Lib/Core.v
index 5af920ae..d664f603 100644
--- a/src/Rupicola/Lib/Core.v
+++ b/src/Rupicola/Lib/Core.v
@@ -1,5 +1,5 @@
 From Coq Require Export
-     Classes.Morphisms Numbers.DecimalString
+     Morphisms DecimalString
      String List ZArith Lia.
 From Coq Require Vector.
 From bedrock2 Require Export
diff --git a/src/Rupicola/Lib/Gensym.v b/src/Rupicola/Lib/Gensym.v
index 91c768d8..ddddd658 100644
--- a/src/Rupicola/Lib/Gensym.v
+++ b/src/Rupicola/Lib/Gensym.v
@@ -1,5 +1,4 @@
-From Coq Require Import
-     String Numbers.DecimalString.
+From Coq Require Import String DecimalString.
 
 Definition _gs (prefix: string) (n: nat) :=
   ("_gs_" ++ prefix ++ NilEmpty.string_of_uint (Nat.to_uint n))%string.
diff --git a/src/Rupicola/Lib/IdentParsing.v b/src/Rupicola/Lib/IdentParsing.v
index dbb54e71..46b79cf2 100644
--- a/src/Rupicola/Lib/IdentParsing.v
+++ b/src/Rupicola/Lib/IdentParsing.v
@@ -1,6 +1,6 @@
 (*! Frontend | Ltac2-based identifier parsing for prettier notations !*)
-Require Import Coq.NArith.NArith Coq.Strings.String.
-Require Import Coq.Init.Byte.
+From Coq Require Import NArith String.
+From Coq.Init Require Import Byte.
 Require Import Ltac2.Ltac2.
 
 Import Ltac2.Init.
diff --git a/src/Rupicola/Lib/Monads.v b/src/Rupicola/Lib/Monads.v
index f8bb01a2..b7225ad0 100644
--- a/src/Rupicola/Lib/Monads.v
+++ b/src/Rupicola/Lib/Monads.v
@@ -1,4 +1,4 @@
-From Coq Require Import Strings.String Logic.FunctionalExtensionality.
+From Coq Require Import String FunctionalExtensionality.
 From Rupicola.Lib Require Import Core.
 
 Set Implicit Arguments.
diff --git a/src/Rupicola/Lib/ToCString.v b/src/Rupicola/Lib/ToCString.v
index 2038f04c..a44270ab 100644
--- a/src/Rupicola/Lib/ToCString.v
+++ b/src/Rupicola/Lib/ToCString.v
@@ -1,8 +1,8 @@
 (* Forked from bedrock2/src/bedrock2/ToCString.v *)
 Require Import bedrock2.Syntax bedrock2.Variables. Import bopname.
 Require Import coqutil.Datatypes.ListSet.
-Require Import Coq.ZArith.BinIntDef Coq.Numbers.BinNums Coq.Numbers.DecimalString.
-Require Import Coq.Strings.String. Local Open Scope string_scope.
+From Coq Require Import BinIntDef BinNums DecimalString.
+From Coq Require Import String. Local Open Scope string_scope.
 
 Definition prelude := "#include <stdint.h>
 #include <string.h>