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

Add changelog entry for Proof using in -noinit mode.
Add changelog entry for Proof using in -noinit mode.
