- **Added:**
  Ltac2 now has a `unify` tactic
  (`#14089 <https://github.com/coq/coq/pull/14089>`_,
  fixes `#14083 <https://github.com/coq/coq/issues/14083>`_,
  by Samuel Gruetter).