• Implement opaque reflection, a feature to allow reflecting functions which call to non-reflected functions #2323.
• Implement reflection from interface files, which can reflect functions from their unfoldings #2326. The feature is limited at the moment by the constraints that affect reflecting functions in general. But we hope it becomes more interesting as reflection is made more flexible.
• Operators in the logic cannot be shadowed locally anymore since #2327.
• Added a flag --dump-pre-normalized-core to show core before A normalization and constraint generation #2336.
• Augmented the context of error messages #2350.
• Add a new flag --etabeta to reason with lambdas in PLE #2356
• Add a new flag --dependentcase to expand support for higher-order reasoning #2384
• Add support for reflecting lambda expressions #2465.
• Enabling the LiquidHaskell plugin now enables -fno-ignore-interface-pragmas (#2326) and -dkeep-comments (#2367).
• LiquidHaskell earned a new --minimal verbosity level as default that prints the banner with the amount of constraints checked (#2395).
  This banner is now suppressed when the verbosity is set to --quiet (#2391).
• Avoid reparsing and retypechecking when verifying modules #2389.
• Name resolution is done only when verifying a module. It is no longer done when importing it #2169. One side effect of this change is that LH can now pick up names in scope using import aliases in most places (but see #2481).
• Allow to link Haskell definitions with logical primitives via define declarations #2463.
• CVC5 solver is now supported for all logical theories, including Sets/Bags #2483