How about "Exported Comments”? These are denoted using TWO consecutive asterisks after the opening bracket, for example (** this is an exported comment *). It signals to a browser that the comment should be included in a DEFINITION module being derived from the module being processed.