From 9ff22cc00f073cf5cab6c37ff8425dd95ae1edad Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 28 Dec 2023 20:45:49 -0500 Subject: [PATCH] closing section --- theories/topology.v | 1 + 1 file changed, 1 insertion(+) 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