From e1ce257a71b065c61ac6f6e3e016486c6a753e35 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 6 Oct 2023 00:32:43 +0900
Subject: [PATCH] fix

---
 theories/normedtype.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/normedtype.v b/theories/normedtype.v
index bb5cec253..c77eaeba3 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -2255,7 +2255,6 @@ Arguments cvgr_neq0 {R V T F FF f}.
 #[global] Hint Extern 0 (ProperFilter _^'+) =>
   (apply: at_right_proper_filter) : typeclass_instances.
 
-
 Section at_left_rightR.
 Variable (R : numFieldType).