From 41b2dd819f903d148c03419b05cedf58620570ba Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sat, 20 Jul 2024 16:25:06 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530

---
 examples/ConsiderDemo.v           |  8 ++++----
 theories/Core/Decision.v          |  2 +-
 theories/Core/EquivDec.v          |  4 ++--
 theories/Data/HList.v             |  2 +-
 theories/Data/List.v              |  5 ++---
 theories/Data/ListFirstnSkipn.v   |  6 +++---
 theories/Data/ListNth.v           |  4 ++--
 theories/Data/Nat.v               |  2 +-
 theories/Data/PreFun.v            |  4 ++--
 theories/Data/SigT.v              |  2 +-
 theories/Data/String.v            |  4 +---
 theories/Programming/Show.v       | 11 +++++------
 theories/Recur/Measure.v          |  6 +++---
 theories/Structures/EqDep.v       |  8 ++++----
 theories/Structures/FunctorLaws.v |  2 +-
 theories/Tactics/EqDep.v          |  4 ++--
 16 files changed, 35 insertions(+), 39 deletions(-)

diff --git a/examples/ConsiderDemo.v b/examples/ConsiderDemo.v
index 542a935d..0da047cf 100644
--- a/examples/ConsiderDemo.v
+++ b/examples/ConsiderDemo.v
@@ -1,10 +1,10 @@
-Require Import Coq.Bool.Bool.
-Require Import Arith.PeanoNat.
+From Coq Require Import Bool.
+From Coq Require Import PeanoNat.
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Data.Nat.
 
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
+From Coq Require Import ZArith.
+From Coq Require Import Lia.
 
 Set Implicit Arguments.
 Set Strict Implicit.
diff --git a/theories/Core/Decision.v b/theories/Core/Decision.v
index c2d29468..e4367e2d 100644
--- a/theories/Core/Decision.v
+++ b/theories/Core/Decision.v
@@ -1,4 +1,4 @@
-Require Import Coq.Classes.DecidableClass.
+From Coq.Classes Require Import DecidableClass.
 
 Definition decideP (P : Prop) {D : Decidable P} : {P} + {~P} :=
   match @Decidable_witness P D as X return (X = true -> P) -> (X = false -> ~P) -> {P} + {~P} with
diff --git a/theories/Core/EquivDec.v b/theories/Core/EquivDec.v
index d02d1f4f..4e4d07f1 100644
--- a/theories/Core/EquivDec.v
+++ b/theories/Core/EquivDec.v
@@ -1,4 +1,4 @@
-Require Import Coq.Classes.EquivDec.
+From Coq.Classes Require Import EquivDec.
 
 Theorem EquivDec_refl_left {T : Type} {c : EqDec T (@eq T)} :
   forall (n : T), equiv_dec n n = left (refl_equal _).
@@ -9,4 +9,4 @@ Proof.
   reflexivity.
 Qed.
 
-Export Coq.Classes.EquivDec.
\ No newline at end of file
+Export EquivDec.
diff --git a/theories/Data/HList.v b/theories/Data/HList.v
index 6ec17186..d0757035 100644
--- a/theories/Data/HList.v
+++ b/theories/Data/HList.v
@@ -1,4 +1,4 @@
-Require Import Coq.Lists.List Coq.Arith.PeanoNat.
+From Coq Require Import List PeanoNat.
 Require Import Relations RelationClasses.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Data.SigT.
diff --git a/theories/Data/List.v b/theories/Data/List.v
index 4de1f73c..f76c7fdf 100644
--- a/theories/Data/List.v
+++ b/theories/Data/List.v
@@ -1,5 +1,4 @@
-Require Import Coq.Lists.List.
-Require Coq.Classes.EquivDec.
+From Coq Require Import List EquivDec.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Structures.Monoid.
 Require Import ExtLib.Structures.Reducible.
@@ -20,7 +19,7 @@ Section EqDec.
   Proof.
     red. unfold Equivalence.equiv, RelationClasses.complement.
     intros.
-    change (x = y -> False) with (x <> y).
+    change (x = y -> False) with (not (x = y)).
     decide equality. eapply EqDec_T.
   Qed.
 End EqDec.
diff --git a/theories/Data/ListFirstnSkipn.v b/theories/Data/ListFirstnSkipn.v
index 33d95cc8..3668804b 100644
--- a/theories/Data/ListFirstnSkipn.v
+++ b/theories/Data/ListFirstnSkipn.v
@@ -1,6 +1,6 @@
-Require Import Coq.Lists.List.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
+From Coq.Lists Require Import List.
+From Coq.ZArith Require Import ZArith.
+From Coq.micromega Require Import Lia.
 
 (** For backwards compatibility with hint locality attributes. *)
 Set Warnings "-unsupported-attributes".
diff --git a/theories/Data/ListNth.v b/theories/Data/ListNth.v
index a4a7c0f4..08ac235f 100644
--- a/theories/Data/ListNth.v
+++ b/theories/Data/ListNth.v
@@ -1,5 +1,5 @@
-Require Import Coq.Lists.List.
-Require Import Coq.Arith.PeanoNat.
+From Coq.Lists Require Import List.
+From Coq.Arith Require Import PeanoNat.
 
 Set Implicit Arguments.
 Set Strict Implicit.
diff --git a/theories/Data/Nat.v b/theories/Data/Nat.v
index 7c81bac2..1bac7527 100644
--- a/theories/Data/Nat.v
+++ b/theories/Data/Nat.v
@@ -1,4 +1,4 @@
-Require Coq.Arith.Arith.
+From Coq.Arith Require Arith.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Structures.Monoid.
 Require Import ExtLib.Tactics.Consider.
diff --git a/theories/Data/PreFun.v b/theories/Data/PreFun.v
index af9cf398..7a26f52e 100644
--- a/theories/Data/PreFun.v
+++ b/theories/Data/PreFun.v
@@ -1,5 +1,5 @@
-Require Import Coq.Classes.Morphisms.
-Require Import Coq.Relations.Relations.
+From Coq.Classes Require Import Morphisms.
+From Coq.Relations Require Import Relations.
 
 Set Implicit Arguments.
 Set Strict Implicit.
diff --git a/theories/Data/SigT.v b/theories/Data/SigT.v
index 0e964658..c0968a19 100644
--- a/theories/Data/SigT.v
+++ b/theories/Data/SigT.v
@@ -1,4 +1,4 @@
-Require Coq.Classes.EquivDec.
+From Coq.Classes Require EquivDec.
 Require Import ExtLib.Structures.EqDep.
 Require Import ExtLib.Tactics.Injection.
 Require Import ExtLib.Tactics.EqDep.
diff --git a/theories/Data/String.v b/theories/Data/String.v
index 954a956c..aa50d65b 100644
--- a/theories/Data/String.v
+++ b/theories/Data/String.v
@@ -1,6 +1,4 @@
-Require Import Coq.Strings.String.
-Require Import Coq.Program.Program. 
-Require Import Coq.Arith.PeanoNat.
+From Coq Require Import String Program PeanoNat.
 
 Require Import ExtLib.Tactics.Consider.
 Require Import ExtLib.Core.RelDec.
diff --git a/theories/Programming/Show.v b/theories/Programming/Show.v
index f0f056f7..e19f4bf2 100644
--- a/theories/Programming/Show.v
+++ b/theories/Programming/Show.v
@@ -1,9 +1,8 @@
-Require Coq.Strings.Ascii.
-Require Coq.Strings.String.
-Require Import Coq.Strings.String.
-Require Import Coq.Program.Wf.
-Require Import Coq.PArith.BinPos.
-Require Import Coq.ZArith.ZArith.
+From Coq Require Ascii.
+From Coq Require Import String.
+From Coq.Program Require Import Wf.
+From Coq Require Import BinPos.
+From Coq Require Import ZArith.
 Require Import ExtLib.Structures.Monoid.
 Require Import ExtLib.Structures.Reducible.
 Require Import ExtLib.Programming.Injection.
diff --git a/theories/Recur/Measure.v b/theories/Recur/Measure.v
index 4ea7847c..0b4368fd 100644
--- a/theories/Recur/Measure.v
+++ b/theories/Recur/Measure.v
@@ -1,5 +1,5 @@
-Require Import Coq.Classes.RelationClasses.
-Require Coq.Arith.Wf_nat.
+From Coq.Classes Require Import RelationClasses.
+From Coq.Arith Require Wf_nat.
 
 Set Implicit Arguments.
 Set Strict Implicit.
@@ -34,4 +34,4 @@ Section measure.
 
   Definition well_founded_mlt : well_founded mlt :=
     @well_founded_compose T nat m lt Wf_nat.lt_wf.
-End measure.
\ No newline at end of file
+End measure.
diff --git a/theories/Structures/EqDep.v b/theories/Structures/EqDep.v
index abfc7015..0df70ef3 100644
--- a/theories/Structures/EqDep.v
+++ b/theories/Structures/EqDep.v
@@ -1,4 +1,4 @@
-Require Coq.Logic.Eqdep_dec.
+From Coq.Logic Require Eqdep_dec.
 Require EquivDec.
 Require Import ExtLib.Core.RelDec.
 Require Import ExtLib.Tactics.Consider.
@@ -12,18 +12,18 @@ Section Classes.
 
   Theorem UIP_refl : forall {x : A} (p1 : x = x), p1 = refl_equal _.
     intros.
-    eapply Coq.Logic.Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
+    eapply Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
   Qed.
 
   Theorem UIP_equal : forall {x y : A} (p1 p2 : x = y), p1 = p2.
-    eapply Coq.Logic.Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
+    eapply Eqdep_dec.UIP_dec. apply EquivDec.equiv_dec.
   Qed.
 
   Lemma inj_pair2 :
     forall (P:A -> Type) (p:A) (x y:P p),
       existT P p x = existT P p y -> x = y.
   Proof.
-    intros. eapply Coq.Logic.Eqdep_dec.inj_pair2_eq_dec; auto.
+    intros. eapply Eqdep_dec.inj_pair2_eq_dec; auto.
   Qed.
 
   Theorem equiv_dec_refl_left : forall a, @EquivDec.equiv_dec _ _ _ dec a a = left eq_refl.
diff --git a/theories/Structures/FunctorLaws.v b/theories/Structures/FunctorLaws.v
index 6397d00f..f706fd63 100644
--- a/theories/Structures/FunctorLaws.v
+++ b/theories/Structures/FunctorLaws.v
@@ -1,4 +1,4 @@
-Require Import Coq.Relations.Relations.
+From Coq.Relations Require Import Relations.
 Require Import ExtLib.Data.Fun.
 Require Import ExtLib.Structures.Functor.
 
diff --git a/theories/Tactics/EqDep.v b/theories/Tactics/EqDep.v
index 2b7a4980..2eba3639 100644
--- a/theories/Tactics/EqDep.v
+++ b/theories/Tactics/EqDep.v
@@ -1,6 +1,6 @@
-Require Import Coq.Classes.EquivDec.
+From Coq.Classes Require Import EquivDec.
 Require Import ExtLib.Structures.EqDep.
-Require Coq.Logic.Eqdep_dec.
+From Coq.Logic Require Eqdep_dec.
 
 Set Implicit Arguments.
 Set Strict Implicit.