clean

math-comp · Oct 14, 2024 · 68c3907 · 68c3907
1 parent c29680a
commit 68c3907
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/theories/normedtype.v b/theories/normedtype.v
@@ -819,7 +819,6 @@ HB.factory Record PseudoMetricNormedZmod_Lmodule_isNormedModule (K : numFieldTyp
 
 HB.builders Context K V of PseudoMetricNormedZmod_Lmodule_isNormedModule K V.
 
-
 (* NB: These lemmas are done latter with more machinery. They should
    be be simplified once normedtype is split, and the present section can
    depend on near lemmas on pseudometricnormedzmodtype ?*)
@@ -945,7 +944,7 @@ Variable (R : rcfType).
 HB.instance Definition _ := GRing.ComAlgebra.copy R R^o.
 #[export, non_forgetful_inheritance]
 HB.instance Definition _ := Vector.copy R R^o.
- #[export, non_forgetful_inheritance]
+#[export, non_forgetful_inheritance]
 HB.instance Definition _ := NormedModule.copy R R^o.
 End rcfType.