fix

math-comp · Oct 5, 2023 · e1ce257 · e1ce257
1 parent 4e6478d
commit e1ce257
Showing 1 changed file with 0 additions and 1 deletion.
diff --git 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).