14.9 Coercions and Sections
14.9 Coercions and Sections
The inheritance mechanism is compatible with the section
mechanism. The global classes and coercions defined inside a section
are redefined after its closing, using their new value and new
type. The classes and coercions which are local to the section are
simply forgotten (no warning message is printed). Just as the
coercions with a local source class or a local target class, and also
coercions which does no more verify the uniform inheritance condition.
Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.3.8.html at 8/10/98