• Optimizations
• Hash-consing
• .vo marshalling
• Representation of identifiers
• General remarks
• ADT "interfaces"
• Adding Eta
• General discussion