closing section

math-comp · Dec 29, 2023 · 9049854 · 9049854
1 parent 84d99f2
commit 9049854
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/theories/topology.v b/theories/topology.v
@@ -8550,3 +8550,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.