diff --git a/theories/topology.v b/theories/topology.v
index 1e9df00075..24bf434984 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -8652,3 +8652,4 @@ apply: (Lh (h a)); first by exists a => //; split => //; exists (a,b).
 by exists b.
 Unshelve. all: by end_near. Qed.
 End cartesian_closed.
+End currying.
\ No newline at end of file