From 8ed2d808b2c9caf022b5e22bb43f2ca6876ebd1b Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 12 Nov 2020 11:49:36 +0100
Subject: Add changelog entry for Proof using in -noinit mode.

---
 doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst

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
new file mode 100644
index 0000000000..9ae759be56
--- /dev/null
+++ 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).
-- 
cgit v1.2.3