From 894b097c41d654be23ddb1b0521e44e13934c177 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 26 Jun 2024 15:33:54 +0200
Subject: [PATCH] changelog for PR 18449

---
 doc/changelog/07-ssreflect/18449-changelog-ssr.rst | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 doc/changelog/07-ssreflect/18449-changelog-ssr.rst

diff --git a/doc/changelog/07-ssreflect/18449-changelog-ssr.rst b/doc/changelog/07-ssreflect/18449-changelog-ssr.rst
new file mode 100644
index 000000000000..713049772efc
--- /dev/null
+++ b/doc/changelog/07-ssreflect/18449-changelog-ssr.rst
@@ -0,0 +1,8 @@
+- **Changed:**
+  The :tacn:`have` tactic generates a proof term containing an opaque
+  constant, as it did up to PR `#15121 <https://github.com/coq/coq/pull/15121>`_
+  included in Coq 8.16.0. See the variant `have @H` to generate a (transparent)
+  let-in instead (:ref:`generating_let_ssr`).
+  (`#18449 <https://github.com/coq/coq/pull/18449>`_,
+  fixes `#18017 <https://github.com/coq/coq/issues/18017>`_,
+  by Enrico Tassi).