Add changelog entry for Proof using in -noinit mode.

coq · Nov 12, 2020 · 8ed2d80 · 8ed2d80
1 parent 403a905
commit 8ed2d80
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst b/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst
@@ -0,0 +1,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).