Adapt to coq/coq#19530

mit-plv · Sep 17, 2024 · 0072da9 · 0072da9
1 parent 941374a
commit 0072da9
Show file tree

Hide file tree

Showing 16 changed files with 31 additions and 32 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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>