fix

Author: mkerjean

theories/hahn_banach_theorem.v

@@ -396,7 +396,8 @@ HB.structure Definition SubConvextvsType (R : numDomainType) (V : lmodType R) (S
 
 
 Section HBGeom.
-
+(*TODO : define on convextvstype once lemmas as continuous_linear_bounded are
+lowered to convextvs *)
 Variable (R : realType) (V : normedModType R) (F : pred V)
 (F' : subLmodType F) (f : {linear F' -> R}).
 
@@ -447,3 +448,5 @@ pose Hg := isLinearContinuous.Build _ _ _ _ g ling contg.
 pose g': {linear_continuous V -> R | *%R} := HB.pack (g : V -> R) Hg.
 by exists g'.
 Qed.
+
+End HBGeom.