doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst


1
2
3
4
5

- **Added:**
  The :cmd:`Proof using` command can now be used without loading the
  Ltac plugin (`-noinit` mode)
  (`#13339 <https://github.com/coq/coq/pull/13339>`_,
  by Théo Zimmermann).