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.