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 `_ + included in Coq 8.16.0. See the variant `have @H` to generate a (transparent) + let-in instead (:ref:`generating_let_ssr`). + (`#18449 `_, + fixes `#18017 `_, + by Enrico Tassi).