Adapt to coq/coq#19530

mit-plv · Sep 17, 2024 · acd0e35 · acd0e35
1 parent ee9653b
commit acd0e35
Show file tree

Hide file tree

Showing 7 changed files with 13 additions and 9 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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) := {