From ac7b295ee1294be99a57950bbf8f82ba73238b3b Mon Sep 17 00:00:00 2001
From: Matt Van Horn <455140+mvanhorn@users.noreply.github.com>
Date: Fri, 24 Apr 2026 03:12:19 -0700
Subject: [PATCH] fix: correct '#[loca]' typo to '#[local]' in
 continuous_path.v

The attribute on Lemma fphi_one was written as '#[loca]' instead of
'#[local]', so unlike the neighboring fphi_zero and fphi_cts lemmas,
fphi_one was not actually marked local.

Fixes #1945.
---
 theories/homotopy_theory/continuous_path.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/homotopy_theory/continuous_path.v b/theories/homotopy_theory/continuous_path.v
index b10955873f..34dca6bb2b 100644
--- a/theories/homotopy_theory/continuous_path.v
+++ b/theories/homotopy_theory/continuous_path.v
@@ -116,7 +116,7 @@ Definition reparameterize := f \o phi.
 #[local] Lemma fphi_zero : reparameterize zero = x.
 Proof. by rewrite /reparameterize /= ?path_zero. Qed.
 
-#[loca] Lemma fphi_one : reparameterize one = y.
+#[local] Lemma fphi_one : reparameterize one = y.
 Proof. by rewrite /reparameterize /= ?path_one. Qed.
 
 #[local] Lemma fphi_cts : continuous reparameterize.