Adapt to https://github.com/coq/coq/pull/19530

convert-hs-to-coq/CSR_preamble.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Local Open Scope Z.
 Require Import riscv.Utility.Utility.
 Local Open Scope alu_scope.

convert-hs-to-coq/Decode_preamble.v

@@ -1,4 +1,4 @@
-Require Coq.ZArith.BinInt.
+From Coq Require BinInt.
 Local Open Scope Z_scope.
 
 Notation Register := BinInt.Z (only parsing).

convert-hs-to-coq/Execute_preamble.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Local Open Scope Z.
 Require Import riscv.Utility.Utility.
 Local Open Scope alu_scope.

src/riscv/Examples/Example64Literal.v

@@ -1,11 +1,11 @@
-Require Import Coq.Lists.List.
+From Coq Require Import List.
 Require Import coqutil.Z.Lia.
 Import ListNotations.
 Require Import coqutil.Word.Naive.
 Require Import coqutil.Word.Properties.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Spec.Decode.
-Require Import Coq.ZArith.BinInt. Local Open Scope Z_scope.
+From Coq Require Import BinInt. Local Open Scope Z_scope.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Platform.Memory.
 Require Import riscv.Platform.Minimal.

src/riscv/Examples/Fib.v

@@ -1,11 +1,11 @@
-Require Import Coq.Lists.List.
+From Coq Require Import List.
 Require Import coqutil.Z.Lia.
 Import ListNotations.
 Require Import coqutil.Word.Naive.
 Require Import coqutil.Word.Properties.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Spec.Decode.
-Require Import Coq.ZArith.BinInt. Local Open Scope Z_scope.
+From Coq Require Import BinInt. Local Open Scope Z_scope.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Platform.Memory.
 Require Import riscv.Platform.Minimal.

src/riscv/Examples/SMTVerif.v

@@ -1,12 +1,12 @@
-Require Import Coq.Lists.List.
-Require Import Coq.Logic.Classical_Prop.
+From Coq Require Import List.
+From Coq Require Import Classical_Prop.
 Import ListNotations.
 Require Import coqutil.Decidable.
 Require Import coqutil.Word.Naive.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Spec.Decode.
 Require Import riscv.Spec.Execute.
-Require Import Coq.ZArith.BinInt. Local Open Scope Z_scope.
+From Coq Require Import BinInt. Local Open Scope Z_scope.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Utility.PowerFunc.
 Require Import riscv.Utility.Monads. Import MonadNotations.

src/riscv/Examples/WMMFree.v

@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List. Import ListNotations.
+From Coq Require Import List. Import ListNotations.
 Require Import coqutil.Decidable.
 Require Import coqutil.Tactics.Tactics.
 Require Import coqutil.Tactics.Simp.
@@ -16,11 +16,11 @@ Require Import coqutil.Map.Z_keyed_SortedListMap.
 Require Import coqutil.Map.OfFunc.
 Require Import coqutil.Word.Properties.
 Require Import coqutil.Z.prove_Zeq_bitwise.
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Require Import riscv.Utility.PowerFunc.
-Require Import Coq.Logic.FunctionalExtensionality.
-Require Import Coq.Logic.PropExtensionality.
-Require Import Coq.derive.Derive.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import PropExtensionality.
+From Coq Require Import Derive.
 Require Import riscv.Spec.Decode.
 
 (* sub-relation *)

src/riscv/Platform/FE310ExtSpec.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Require Import coqutil.Map.Interface.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Platform.MinimalMMIO.

src/riscv/Platform/LogInstructionTrace.v

@@ -1,5 +1,5 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import List.
 Require Import riscv.Utility.Monads. Import StateAbortFailOperations.
 Require Import riscv.Utility.MonadNotations.
 Require Import riscv.Spec.Decode.

src/riscv/Platform/Memory.v

@@ -1,5 +1,5 @@
-Require Import Coq.Lists.List.
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import List.
+From Coq Require Import ZArith.
 Require Import coqutil.Word.Interface.
 Require Import coqutil.Word.Properties.
 Require Import coqutil.Word.Bitwidth.

src/riscv/Platform/MetricLogging.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import coqutil.Z.Lia.
 
 Section Riscv.

src/riscv/Platform/MetricMaterializeRiscvProgram.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Require Import coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Import riscv.Utility.Monads.
 Require Import riscv.Utility.FreeMonad.

src/riscv/Platform/MetricMinimal.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Monads. Import OStateOperations.
 Require Import riscv.Utility.MonadNotations.
 Require Import riscv.Spec.Decode.
@@ -16,8 +16,8 @@ Require Import riscv.Platform.MetricLogging.
 Require Import riscv.Spec.MetricPrimitives.
 Require Import coqutil.Z.Lia.
 Require Import coqutil.Z.Lia.
-Require Import Coq.Logic.FunctionalExtensionality.
-Require Import Coq.Logic.PropExtensionality.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import PropExtensionality.
 
 Local Open Scope Z_scope.
 Local Open Scope bool_scope.

src/riscv/Platform/MetricMinimalMMIO.v

@@ -1,14 +1,14 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Logic.FunctionalExtensionality.
-Require Import Coq.Logic.PropExtensionality.
+From Coq Require Import ZArith.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import PropExtensionality.
 Require Import riscv.Utility.Monads.
 Require Import riscv.Utility.MonadNotations.
 Require Import riscv.Spec.Decode.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Spec.Primitives.
 Require Import riscv.Spec.MetricPrimitives.
-Require Import Coq.Lists.List. Import ListNotations.
+From Coq Require Import List. Import ListNotations.
 Require Export riscv.Platform.RiscvMachine.
 Require Export riscv.Platform.MetricRiscvMachine.
 Require Import riscv.Platform.MinimalMMIO.

src/riscv/Platform/MetricRiscvMachine.v

@@ -1,4 +1,4 @@
-Require Import Coq.Strings.String.
+From Coq Require Import String.
 Require Import coqutil.Map.Interface.
 Require Import coqutil.Word.Interface.
 Require Import coqutil.Word.LittleEndian.

src/riscv/Platform/MetricSane.v

@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List.
+From Coq Require Import List.
 Require Import coqutil.Map.Interface coqutil.Map.Properties.
 Require Import coqutil.Tactics.Tactics.
 Require Import riscv.Spec.Machine.

src/riscv/Platform/Minimal.v

@@ -1,7 +1,7 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
-Require Import Coq.Logic.FunctionalExtensionality.
-Require Import Coq.Logic.PropExtensionality.
+From Coq Require Import ZArith.
+From Coq Require Import List.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import PropExtensionality.
 Require Import riscv.Utility.Monads. Import OStateOperations.
 Require Import riscv.Utility.MonadNotations.
 Require Import riscv.Spec.Decode.

src/riscv/Platform/MinimalCSRs.v

@@ -1,6 +1,6 @@
-Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope.
-Require Import Coq.Strings.String.
-Require Import Coq.Lists.List. Import ListNotations.
+From Coq Require Import ZArith. Local Open Scope Z_scope.
+From Coq Require Import String.
+From Coq Require Import List. Import ListNotations.
 Require Import coqutil.Tactics.Tactics.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Platform.Memory.

src/riscv/Platform/MinimalCSRsDet.v

@@ -1,5 +1,5 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List.
+From Coq Require Import ZArith.
+From Coq Require Import List.
 Require Import riscv.Utility.Monads. Import StateAbortFailOperations.
 Require Import riscv.Utility.MonadNotations.
 Require Import riscv.Spec.Decode.

src/riscv/Platform/MinimalLogging.v

@@ -1,5 +1,5 @@
-Require Import Coq.ZArith.BinInt.
-Require Import Coq.Strings.String.
+From Coq Require Import BinInt.
+From Coq Require Import String.
 Require Import riscv.Utility.Monads. Import OStateOperations.
 Require Import riscv.Utility.MonadNotations.
 Require Import riscv.Spec.Decode.
@@ -8,7 +8,7 @@ Require Import riscv.Spec.Machine.
 Require Import riscv.Spec.Execute.
 Require Import riscv.Utility.PowerFunc.
 Require Import riscv.Utility.Utility.
-Require Import Coq.Lists.List. Import ListNotations.
+From Coq Require Import List. Import ListNotations.
 Require Import riscv.Platform.Minimal.
 Require Import coqutil.Map.Interface.
 

src/riscv/Platform/MinimalMMIO.v

@@ -1,13 +1,13 @@
-Require Import Coq.Strings.String.
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import String.
+From Coq Require Import ZArith.
 Require Import riscv.Utility.Monads.
 Require Import riscv.Utility.MonadNotations.
 Require Export riscv.Utility.FreeMonad.
 Require Import riscv.Spec.Decode.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Spec.Primitives.
-Require Import Coq.Lists.List. Import ListNotations.
+From Coq Require Import List. Import ListNotations.
 Require Import coqutil.Datatypes.List.
 Require Import coqutil.Datatypes.ListSet.
 Require Export riscv.Platform.RiscvMachine.

src/riscv/Platform/MinimalMMIO_Post.v

@@ -1,12 +1,12 @@
-Require Import Coq.Strings.String.
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import String.
+From Coq Require Import ZArith.
 Require Import riscv.Utility.Monads.
 Require Import riscv.Utility.MonadNotations.
 Require Import riscv.Spec.Decode.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Spec.Primitives.
-Require Import Coq.Lists.List. Import ListNotations.
+From Coq Require Import List. Import ListNotations.
 Require Import coqutil.Datatypes.List.
 Require Import coqutil.Datatypes.ListSet.
 Require Export riscv.Platform.RiscvMachine.

src/riscv/Platform/RiscvMachine.v

@@ -1,5 +1,5 @@
-Require Import Coq.Strings.String.
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import String.
+From Coq Require Import BinInt.
 Require Import coqutil.Map.Interface.
 Require Import coqutil.Word.Interface.
 Require Import coqutil.Word.LittleEndian.

src/riscv/Platform/Run.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import coqutil.Word.LittleEndian.
 Require Import riscv.Utility.Monads.
 Require Import riscv.Utility.MonadNotations.

src/riscv/Platform/Sane.v

@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List.
+From Coq Require Import List.
 Require Import coqutil.Map.Interface coqutil.Map.Properties.
 Require Import coqutil.Tactics.Tactics.
 Require Import riscv.Spec.Machine.

src/riscv/Proofs/DecodeByExtension.v

@@ -1,5 +1,5 @@
-Require Export Coq.ZArith.ZArith.
-Require Export Coq.Lists.List. Import ListNotations.
+From Coq Require Export ZArith.
+From Coq Require Export List. Import ListNotations.
 Require Import coqutil.Tactics.Tactics.
 Require Import coqutil.Tactics.rdelta.
 Require Import coqutil.Tactics.destr.

src/riscv/Proofs/DecodeEncodeProver.v

@@ -1,5 +1,5 @@
-Require Export Coq.ZArith.ZArith.
-Require Export Coq.Lists.List. Import ListNotations.
+From Coq Require Export ZArith.
+From Coq Require Export List. Import ListNotations.
 Require Export riscv.Spec.Decode.
 Require Export riscv.Utility.Encode.
 Require Export riscv.Utility.Utility.

src/riscv/Proofs/EncodeBound.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith.
+From Coq Require Import ZArith.
 Require Import riscv.Spec.Decode.
 Require Import riscv.Utility.Encode.
 Require Import riscv.Utility.Utility.

src/riscv/Proofs/EncodeDecode.v

@@ -1,5 +1,5 @@
-Require Export Coq.ZArith.ZArith.
-Require Export Coq.Lists.List. Import ListNotations.
+From Coq Require Export ZArith.
+From Coq Require Export List. Import ListNotations.
 Require Import coqutil.Tactics.rdelta.
 Require Import coqutil.Tactics.destr.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/InstructionSetOrder.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.ZArith. Open Scope Z_scope.
+From Coq Require Import ZArith. Open Scope Z_scope.
 Require Import coqutil.Z.Lia.
 Require Import riscv.Spec.Decode.
 Require Import riscv.Utility.Encode.

src/riscv/Proofs/VerifyDecode.v

@@ -1,5 +1,5 @@
-Require Export Coq.ZArith.ZArith.
-Require Export Coq.Lists.List. Import ListNotations.
+From Coq Require Export ZArith.
+From Coq Require Export List. Import ListNotations.
 Require Import coqutil.Tactics.rdelta.
 Require Import coqutil.Tactics.destr.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_Fence.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_FenceI.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_I.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_I_shift_57.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_I_shift_66.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_I_system.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_R.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_R_atomic.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_S.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_SB.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_U.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.

src/riscv/Proofs/invert_encode_UJ.v

@@ -1,4 +1,4 @@
-Require Import Coq.ZArith.BinInt.
+From Coq Require Import BinInt.
 Require Import riscv.Utility.Encode.
 Require Import coqutil.Z.BitOps.
 Require Import coqutil.Z.prove_Zeq_bitwise.