doc/changelog/02-specification-language/13183-using-att.rst


1
2
3
4
5
6

- **Added:**
  Definition and (Co)Fixpoint now support the :attr:`using` attribute.
  It has the same effect as :cmd:`Proof using`, which is only available in
  interactive mode.
  (`#13183 <https://github.com/coq/coq/pull/13183>`_,
  by Enrico Tassi).