• Organization
• Participants
• Polymorphic universes
• Projections
• Tactics and new proof engine
• Windows and MacOS packages
• Naming and parsing existential variables
• simpl vs cbn
• Miscellaneous