From 7514a81277b6f0bd58f0eff851b5f8a454358421 Mon Sep 17 00:00:00 2001 From: zstone Date: Wed, 22 Mar 2023 15:57:41 -0400 Subject: [PATCH] fixing build --- theories/cantor.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/cantor.v b/theories/cantor.v index 62e8bcb6e1..35c2ea1d14 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -695,4 +695,4 @@ have : set_surj [set: cantor_space] [set: T] (cst point). by move=> q _; exists point => //; have /negP := xpt q; rewrite negbK => /eqP. by case/Psurj => f cstf; exists f; rewrite -cstf; apply: cst_continuous. Qed. -Section alexandroff_hausdorff. \ No newline at end of file +End alexandroff_hausdorff. \ No newline at end of file