fix

Author: affeldt-aist

theories/normedtype_theory/tvs.v

@@ -679,7 +679,7 @@ HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.typ
     continuousP : continuous f
   }.
 
-HB.builders Context K E F s f of @isLinearContinuous K E F s f.
+HB.builders Context K E F s f & @isLinearContinuous K E F s f.
 
 HB.instance Definition _ := GRing.isLinear.Build K E F s f linearP.
 HB.instance Definition _ := isContinuous.Build E F f continuousP.