diff --git a/classic/util/bigcat.v b/classic/util/bigcat.v
index 28051b558678083acb7c18007400d0f16bb7e761..d4ecebcf55a39696e78ad097a8a549971871c86f 100644
--- a/classic/util/bigcat.v
+++ b/classic/util/bigcat.v
@@ -1,4 +1,4 @@
-From rt.util Require Export bigcat.
+Require Export rt.util.bigcat.
 
 Require Import rt.classic.util.tactics rt.classic.util.notation rt.classic.util.bigord.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/classic/util/counting.v b/classic/util/counting.v
index d5819583b177450399fd69765a4ec6976c2699b2..a1710fc021d9ccbe5712d4363870fe3c2992a130 100644
--- a/classic/util/counting.v
+++ b/classic/util/counting.v
@@ -1,4 +1,4 @@
-From rt.util Require Export counting.
+Require Export rt.util.counting.
 
 Require Import rt.classic.util.tactics rt.classic.util.ord_quantifier.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/classic/util/div_mod.v b/classic/util/div_mod.v
index 40f21993e7f0c567d61d88be50788c2b794a73ba..309763248979239dda1fc406a3dab61cdcef643a 100644
--- a/classic/util/div_mod.v
+++ b/classic/util/div_mod.v
@@ -1,4 +1,4 @@
-From rt.util Require Export div_mod.
+Require Export rt.util.div_mod.
 
 Require Import Arith Omega Nat.
 Require Import rt.classic.util.tactics rt.util.ssromega rt.classic.util.nat.
diff --git a/classic/util/list.v b/classic/util/list.v
index b8d7d06f12c9590bb0e5fd093ab9ab09bd2086ee..224fda93f79e5b1ddf4f434065f7e220b0fb90d8 100644
--- a/classic/util/list.v
+++ b/classic/util/list.v
@@ -1,4 +1,4 @@
-From rt.util Require Export list.
+Require Export rt.util.list.
 
 Require Import rt.classic.util.tactics.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
diff --git a/classic/util/nat.v b/classic/util/nat.v
index 8359327eefabb9894f8bbbaa16590bccb511b565..e12a2c24f989ca7f55f9ecb2fe26474596c26929 100644
--- a/classic/util/nat.v
+++ b/classic/util/nat.v
@@ -1,4 +1,4 @@
-From rt.util Require Export nat.
+Require Export rt.util.nat.
 
 Require Import rt.classic.util.tactics rt.util.ssromega.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
diff --git a/classic/util/notation.v b/classic/util/notation.v
index f0e803df8800e6f298b0c8c23f1c2e3a0ef6e097..eacc5be9e3a413cec9122302167e23f4ded5fe95 100644
--- a/classic/util/notation.v
+++ b/classic/util/notation.v
@@ -1,4 +1,4 @@
-From rt.util Require Export notation.
+Require Export rt.util.notation.
 
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
diff --git a/classic/util/seqset.v b/classic/util/seqset.v
index e1f3e366a905173d53e7ddbfe3a8157b61baabc9..648f03c2b50e2e5bdf0b31bfe59667d1089788f2 100644
--- a/classic/util/seqset.v
+++ b/classic/util/seqset.v
@@ -1,4 +1,4 @@
-From rt.util Require Export seqset.
+Require Export rt.util.seqset.
 
 From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq fintype.
 
diff --git a/classic/util/step_function.v b/classic/util/step_function.v
index 9cbfd3e09ca71db4af9110449de467096fa112f6..447e03b76a26a5dacf3ba9bda95a2e5707a44d13 100644
--- a/classic/util/step_function.v
+++ b/classic/util/step_function.v
@@ -1,4 +1,4 @@
-From rt.util Require Export step_function.
+Require Export rt.util.step_function.
 
 Require Import rt.classic.util.tactics rt.classic.util.notation rt.classic.util.induction.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
diff --git a/classic/util/sum.v b/classic/util/sum.v
index 6ed29caef71840b42ee0bb7c4765c9cfe9f849dd..149025e13dcb2618f5f8effae5d1ff4c952aa9c7 100644
--- a/classic/util/sum.v
+++ b/classic/util/sum.v
@@ -1,6 +1,10 @@
-From rt.util Require Export sum ssromega.
+Require Export rt.util.sum.
+Require Export rt.util.ssromega.
 
-From rt.classic.util Require Import tactics notation sorting nat.
+Require Import rt.classic.util.tactics.
+Require Import rt.classic.util.notation.
+Require Import rt.classic.util.sorting.
+Require Import rt.classic.util.nat.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
 
 (* Lemmas about sum. *)
diff --git a/classic/util/tactics.v b/classic/util/tactics.v
index ed5a0e6c5006adc9262781155a515f8dca047d6b..43182e49d3ab4aace3b03fabbaf5c3f2df0da9c2 100644
--- a/classic/util/tactics.v
+++ b/classic/util/tactics.v
@@ -1,4 +1,4 @@
-From rt.util Require Export tactics.
+Require Export rt.util.tactics.
 
 (* *********************************************************************)
 (*                                                                     *)
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index 9f272f67ef4f843d9f1e79d8c7655db189660c68..9dde5da286f048631dc5bfe8a081387c24ff69aa 100644
--- a/util/nondecreasing.v
+++ b/util/nondecreasing.v
@@ -1,4 +1,8 @@
-From rt.util Require Import epsilon nat list tactics ssromega.
+Require Import rt.util.epsilon.
+Require Import rt.util.nat.
+Require Import rt.util.list.
+Require Import rt.util.tactics.
+Require Import rt.util.ssromega.
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (** * Non-Decreasing Sequence and Distances *)
diff --git a/util/search_arg.v b/util/search_arg.v
index 33e70b5951bcac6bcea40101dbbd3c8bb2ab0033..555c06df937ef9a46bd3d747e8c0519810d5531b 100644
--- a/util/search_arg.v
+++ b/util/search_arg.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
-From rt.util Require Import tactics.
+Require Import rt.util.tactics.
 
 (** This file introduces a function called search_arg that allows finding the
     argument within a given range for which a function is minimal w.r.t. to a
diff --git a/util/sum.v b/util/sum.v
index d34d20e6c9c81db9d793619a1adb1745aee09d04..6bde1f64a0603e82163483e541c9ec7264e9fff5 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -1,4 +1,8 @@
-From rt.util Require Import tactics notation nat ssromega. 
+Require Import rt.util.tactics.
+Require Import rt.util.notation.
+Require Import rt.util.nat.
+Require Import rt.util.ssromega.
+
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
 
 (* Lemmas about sum. *)