Adapt to rocq-prover/rocq#19530

Author: proux01

src/Common.v

@@ -1,5 +1,5 @@
 Require Import Coq.Lists.List.
-Require Import Coq.ZArith.ZArith Coq.Lists.SetoidList.
+From Coq Require Import ZArith.ZArith SetoidList.
 Require Export Coq.Setoids.Setoid Coq.Classes.RelationClasses
         Coq.Program.Program Coq.Classes.Morphisms.
 Require Export Fiat.Common.Tactics.SplitInContext.

src/Common/Equality.v

@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List Coq.Lists.SetoidList.
+From Coq Require Import List SetoidList.
 Require Import Coq.Bool.Bool.
 Require Import Coq.Arith.PeanoNat.
 Require Import Coq.Strings.Ascii.

src/Common/List/FlattenList.v

@@ -1,4 +1,5 @@
-Require Import Coq.Lists.List Coq.Lists.SetoidList Fiat.Common.
+From Coq Require Import List SetoidList.
+Require Import Fiat.Common.
 Require Import Coq.Arith.Arith.
 
 Unset Implicit Arguments.

src/Common/List/ListFacts.v

@@ -1,7 +1,7 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Require Import Coq.ZArith.ZArith.
-Require Import Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool
-        Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts.
+From Coq Require Import List SetoidList Bool.
+Require Import Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts.
 
 Unset Implicit Arguments.
 

src/Common/List/PermutationFacts.v

@@ -220,7 +220,7 @@ Proof.
   apply Permutation_length_1 in H; congruence.
 Qed.
 
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import SetoidList.
 
 Lemma InA_app_swap {A} eqA :
   Equivalence eqA

src/Common/Wf.v

@@ -1,6 +1,9 @@
 (** * Miscellaneous Well-Foundedness Facts *)
-Require Import Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf.
-Require Import Coq.Lists.SetoidList.
+From Coq Require Import Setoid.
+From Coq.Program Require Import Program Wf.
+From Coq Require Import Wf_nat Morphisms.
+From Coq.Init Require Import Wf.
+From Coq Require Import SetoidList.
 Require Import Coq.Arith.PeanoNat.
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 

src/Computation/Decidable.v

@@ -139,7 +139,7 @@ Global Program Instance bool_eq_Decidable {n m : bool} : Decidable (n = m) := {
 Obligation 1. t' eqb_true_iff. Qed.
 
 Require Import Coq.Strings.Ascii.
-Require Import Coq.Bool.Sumbool.
+From Coq Require Import Sumbool.
 
 Global Program Instance ascii_eq_Decidable {n m : Ascii.ascii} :
   Decidable (n = m) := {