Adapt to coq/coq#19530

coq-community · Sep 16, 2024 · 793d43b · 793d43b
1 parent da515d5
commit 793d43b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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.