rename homotopy_theory/path.v

math-comp · Dec 4, 2024 · f788745 · f788745
1 parent 47e0e0f
commit f788745
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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 → theories/homotopy_theory/continuous_path.v b/theories/homotopy_theory/path.v → theories/homotopy_theory/continuous_path.v
diff --git 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.