doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst


1
2
3
4
5
6

- **Added:**
  The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to
  give a name to the old value so as to be able to reuse it inside the
  new one
  (`#11503 <https://github.com/coq/coq/pull/11503>`_,
  by Pierre-Marie Pédrot).