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


1
2
3
4
5
6

- **Added:**
  Attribute :attr:`using` now supported by Definition and (Co)Fixpoint.
  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).