From 793d43bf64068f7f316ae565ec3c0f81934123bf Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Sun, 21 Jul 2024 10:41:49 +0200
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530

---
 theories/Autosubst_Basics.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Autosubst_Basics.v b/theories/Autosubst_Basics.v
index 1940c3b..d1dea83 100644
--- a/theories/Autosubst_Basics.v
+++ b/theories/Autosubst_Basics.v
@@ -4,8 +4,8 @@
   substitutions.
 *)
 
-Require Import Coq.Program.Tactics.
-Require Import Coq.Arith.PeanoNat List FunctionalExtensionality.
+From Coq.Program Require Import Tactics.
+From Coq Require Import PeanoNat List FunctionalExtensionality.
 
 (** Annotate "a" with additional information. *)
 Definition annot {A B} (a : A) (b : B) : A := a.