update doc

Author: affeldt-aist

theories/convex.v

@@ -14,10 +14,12 @@ From HB Require Import structures.
 (* completed with material from infotheo.                                     *)
 (*                                                                            *)
 (*   isConvexSpace R T == interface for convex spaces                         *)
-(*       ConvexSpace R == structure of convex space                           *)
+(*                        The HB class is ConvexSpace.                        *)
 (*         a <| t |> b == convexity operator                                  *)
-(* E : lmodType R with R : realDomainType and R : realDomainType are shown to *)
-(* be convex spaces                                                           *)
+(*                                                                            *)
+(* * instances of convex space:                                               *)
+(*   E : lmodType R with R : realDomainType, R : realDomainType,              *)
+(*   R : realFieldType, R : realType                                          *)
 (*                                                                            *)
 (******************************************************************************)