- Skim through an introduction to decidability of higher-order matching
- String interpolator macros were ported to work at compile-time
- Improve stability of the codebase (with respect to Dotty)
- Add missing tactic building blocks (repetition and fallback)
- Better interoperability between the front and the kernel theory
- The front relies on its own invariants to ensure a successful kernel reconstruction
- lampepfl/dotty#14907