Merge PR coq#19280: changelog for PR 18449

Reviewed-by: proux01 Ack-by: ybertot Co-authored-by: proux01 <[email protected]>
SkySkimmer · Jun 27, 2024 · c8709fd · c8709fd
2 parents 27085c3 + 894b097
commit c8709fd
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/doc/changelog/07-ssreflect/18449-changelog-ssr.rst 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).