From be51c8ef5312ab9320421833f6c023ce19459f22 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 14 Oct 2020 11:20:57 +0200
Subject: Document the changes.

---
 doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst

diff --git a/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst b/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst
new file mode 100644
index 0000000000..1a6bc88c6c
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  When declaring arbitrary terms as hints, unsolved
+  evars are not abstracted implicitly anymore and instead
+  raise an error
+  (`#13139 <https://github.com/coq/coq/pull/13139>`_,
+  by Pierre-Marie Pédrot).
-- 
cgit v1.2.3