closing section

math-comp · Jan 14, 2024 · 9ff22cc · 9ff22cc
1 parent 733ebab
commit 9ff22cc
Showing 1 changed file with 1 addition and 0 deletions.
diff --git 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.