diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 7a5228a1c..56017a4e2 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -65,6 +65,8 @@
 - in `probability.v`:
   + `integral_distribution` -> `ge0_integral_distribution`
 
+- file `homotopy_theory/path.v` -> `homotopy_theory/continuous_path.v`
+
 ### Generalized
 
 - in `probability.v`:
diff --git a/_CoqProject b/_CoqProject
index 882574185..bf4dcb863 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -63,7 +63,7 @@ theories/topology_theory/sigT_topology.v
 
 theories/homotopy_theory/homotopy.v
 theories/homotopy_theory/wedge_sigT.v
-theories/homotopy_theory/path.v
+theories/homotopy_theory/continuous_path.v
 
 theories/separation_axioms.v
 theories/function_spaces.v
diff --git a/theories/Make b/theories/Make
index d82042d37..de272b231 100644
--- a/theories/Make
+++ b/theories/Make
@@ -31,7 +31,7 @@ topology_theory/sigT_topology.v
 
 homotopy_theory/homotopy.v
 homotopy_theory/wedge_sigT.v
-homotopy_theory/path.v
+homotopy_theory/continuous_path.v
 
 separation_axioms.v
 function_spaces.v
diff --git a/theories/homotopy_theory/path.v b/theories/homotopy_theory/continuous_path.v
similarity index 100%
rename from theories/homotopy_theory/path.v
rename to theories/homotopy_theory/continuous_path.v
diff --git a/theories/homotopy_theory/homotopy.v b/theories/homotopy_theory/homotopy.v
index d424c7b38..381b6bcba 100644
--- a/theories/homotopy_theory/homotopy.v
+++ b/theories/homotopy_theory/homotopy.v
@@ -1,3 +1,3 @@
 (* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Export wedge_sigT.
-From mathcomp Require Export path.
+From mathcomp Require Export continuous_path.