From 4063f04f5c3605ad06b8a476e2300505cab1ca5d Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 17 Sep 2024 09:37:46 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530 (#113)

---
 src/Common.v                       | 2 +-
 src/Common/Equality.v              | 2 +-
 src/Common/List/FlattenList.v      | 3 ++-
 src/Common/List/ListFacts.v        | 4 ++--
 src/Common/List/PermutationFacts.v | 2 +-
 src/Common/Wf.v                    | 7 +++++--
 src/Computation/Decidable.v        | 2 +-
 7 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/src/Common.v b/src/Common.v
index 758fac871..441073064 100644
--- a/src/Common.v
+++ b/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.
diff --git a/src/Common/Equality.v b/src/Common/Equality.v
index ac9498281..75102520d 100644
--- a/src/Common/Equality.v
+++ b/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.
diff --git a/src/Common/List/FlattenList.v b/src/Common/List/FlattenList.v
index 74c46cd3e..5165f86b5 100644
--- a/src/Common/List/FlattenList.v
+++ b/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.
diff --git a/src/Common/List/ListFacts.v b/src/Common/List/ListFacts.v
index 09c578432..02d4eb956 100644
--- a/src/Common/List/ListFacts.v
+++ b/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.
 
diff --git a/src/Common/List/PermutationFacts.v b/src/Common/List/PermutationFacts.v
index c4e7f7304..357cb15fe 100644
--- a/src/Common/List/PermutationFacts.v
+++ b/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
diff --git a/src/Common/Wf.v b/src/Common/Wf.v
index 9be4543dc..0beffb173 100644
--- a/src/Common/Wf.v
+++ b/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.
 
diff --git a/src/Computation/Decidable.v b/src/Computation/Decidable.v
index 027d6d4c6..9bfaf7d58 100644
--- a/src/Computation/Decidable.v
+++ b/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) := {