"Yannick Duch�ne (Hibou57)" wrote in message news:op.vc0hbmfnxmjfy8@garhos... >Le Thu, 20 May 2010 13:03:01 +0200, Gavino a �crit: >> It's to avoid overloading, especially the implicit declaration of >> user-defined subprograms. >While this only occurs with tagged types, and SPARK 95 has support for >tagged type. Or may be I'm wrong somewhere, or else, I did not understood >what you were to say. Firstly, derived types can introduce overloaded enumeration literals, which SPARK prohibits. Secondly, if the parent type is one declared immediately within the visible part of a package, then certain subprograms declared there are implicitly declared for the derived type, again a form of overloading.