From 3153d22a9d460f66b6bd70fa722be28203ddbd97 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Wed, 4 Dec 2024 23:25:05 +0900
Subject: [PATCH] rename homotopy_theory/path.v

---
 CHANGELOG_UNRELEASED.md                                | 2 ++
 _CoqProject                                            | 2 +-
 theories/Make                                          | 2 +-
 theories/homotopy_theory/{path.v => continuous_path.v} | 0
 theories/homotopy_theory/homotopy.v                    | 2 +-
 5 files changed, 5 insertions(+), 3 deletions(-)
 rename theories/homotopy_theory/{path.v => continuous_path.v} (100%)

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.