From b2710e271e5346d6ccd2f77c55c2a040ef08bee9 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 24 Jul 2024 14:23:52 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530

---
 hoare_example/Imp.v        |  6 +++---
 theories/Axioms.v          | 14 +++++++-------
 theories/Core/KTreeFacts.v |  6 +++---
 theories/Eq/Eqit.v         |  2 +-
 theories/Props/Finite.v    |  2 +-
 theories/Props/Leaf.v      |  2 +-
 tutorial/Asm.v             |  8 +++++---
 tutorial/Imp.v             |  6 +++---
 tutorial/Imp2Asm.v         |  2 +-
 tutorial/Utils_tutorial.v  |  6 +++---
 10 files changed, 28 insertions(+), 26 deletions(-)

diff --git a/hoare_example/Imp.v b/hoare_example/Imp.v
index de66c30e..53f83807 100644
--- a/hoare_example/Imp.v
+++ b/hoare_example/Imp.v
@@ -40,9 +40,9 @@
 
 (* begin hide *)
 From Coq Require Import
-     Arith.PeanoNat
-     Lists.List
-     Strings.String
+     PeanoNat
+     List
+     String
      Morphisms
      Setoid
      RelationClasses.
diff --git a/theories/Axioms.v b/theories/Axioms.v
index 2efd869b..9419afa1 100644
--- a/theories/Axioms.v
+++ b/theories/Axioms.v
@@ -3,16 +3,16 @@
 (** Other ITree modules should import this to avoid accidentally using more
    axioms elsewhere. *)
 
-From Coq Require Import
-  Logic.Classical_Prop
-  Logic.ClassicalChoice
-  Logic.EqdepFacts
-  Logic.FunctionalExtensionality
+From Coq.Logic Require Import
+  Classical_Prop
+  ClassicalChoice
+  EqdepFacts
+  FunctionalExtensionality
 .
 
 (* Must be imported to use [ddestruction] *)
-From Coq Require Export
-  Program.Equality
+From Coq.Program Require Export
+  Equality
 .
 
 Set Implicit Arguments.
diff --git a/theories/Core/KTreeFacts.v b/theories/Core/KTreeFacts.v
index a84858e8..0bc1a29c 100644
--- a/theories/Core/KTreeFacts.v
+++ b/theories/Core/KTreeFacts.v
@@ -2,9 +2,9 @@
 
 (* begin hide *)
 From Coq Require Import
-     Classes.Morphisms
-     Setoids.Setoid
-     Relations.Relations.
+     Morphisms
+     Setoid
+     Relations.
 
 From Paco Require Import paco.
 
diff --git a/theories/Eq/Eqit.v b/theories/Eq/Eqit.v
index 9ec83997..ad7aac78 100644
--- a/theories/Eq/Eqit.v
+++ b/theories/Eq/Eqit.v
@@ -18,7 +18,7 @@
 Set Warnings "-deprecated-hint-rewrite-without-locality".
 
 From Coq Require Import
-     Structures.Orders (* Hint Unfold is_true *)
+     Orders (* Hint Unfold is_true *)
      Program
      Setoid
      Morphisms
diff --git a/theories/Props/Finite.v b/theories/Props/Finite.v
index d803c230..cce8f26f 100644
--- a/theories/Props/Finite.v
+++ b/theories/Props/Finite.v
@@ -10,7 +10,7 @@ From ITree Require Import
 From ITree.Events Require Import Nondeterminism Exception. (* For counterexamples *)
 
 From Paco Require Import paco.
-From Coq Require Import Morphisms Basics Program.Equality.
+From Coq Require Import Morphisms Basics Equality.
 Import ITree.
 Import ITreeNotations.
 Import LeafNotations.
diff --git a/theories/Props/Leaf.v b/theories/Props/Leaf.v
index aebbb2e3..aecdda68 100644
--- a/theories/Props/Leaf.v
+++ b/theories/Props/Leaf.v
@@ -13,7 +13,7 @@ From ITree Require Import
      Props.HasPost.
 
 From Paco Require Import paco.
-From Coq Require Import Morphisms Basics Program.Equality.
+From Coq Require Import Morphisms Basics Equality.
 Import ITree.
 Import ITreeNotations.
 (* end hide *)
diff --git a/tutorial/Asm.v b/tutorial/Asm.v
index 410fe4fd..dd4816be 100644
--- a/tutorial/Asm.v
+++ b/tutorial/Asm.v
@@ -6,9 +6,11 @@
 
 (* begin hide *)
 From Coq Require Import
-     Strings.String
-     Program.Basics
-     ZArith.ZArith
+     String.
+From Coq.Program Require Import
+     Basics.
+From Coq Require Import
+     ZArith
      Morphisms
      Setoid
      RelationClasses.
diff --git a/tutorial/Imp.v b/tutorial/Imp.v
index ef832efc..c456acc3 100644
--- a/tutorial/Imp.v
+++ b/tutorial/Imp.v
@@ -40,9 +40,9 @@
 
 (* begin hide *)
 From Coq Require Import
-     Arith.PeanoNat
-     Lists.List
-     Strings.String
+     PeanoNat
+     List
+     String
      Morphisms
      Setoid
      RelationClasses.
diff --git a/tutorial/Imp2Asm.v b/tutorial/Imp2Asm.v
index 612f1194..605799fd 100644
--- a/tutorial/Imp2Asm.v
+++ b/tutorial/Imp2Asm.v
@@ -26,7 +26,7 @@ From Coq Require Import
      Morphisms
      Setoid
      Decimal
-     Numbers.DecimalString
+     DecimalString
      ZArith
      RelationClasses.
 
diff --git a/tutorial/Utils_tutorial.v b/tutorial/Utils_tutorial.v
index c9e0eacb..3136d2f1 100644
--- a/tutorial/Utils_tutorial.v
+++ b/tutorial/Utils_tutorial.v
@@ -16,11 +16,11 @@
 (* begin hide *)
 From Coq Require Import
      Ascii
-     Strings.String
+     String
      List
-     Arith.Arith
+     Arith
      ZArith
-     Nat 
+     Nat
      Psatz.
 
 From ExtLib Require Import