doc/changelog/04-tactics/14089-ltac2_unify.rst


1
2
3
4
5

- **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).