From fafc731885f84656ec884d40b843aa62a5991025 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 30 Mar 2020 13:34:17 +0200
Subject: Include review suggestions

---
 .../02-specification-language/11579-inductive-params.rst      | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'doc')

diff --git a/doc/changelog/02-specification-language/11579-inductive-params.rst b/doc/changelog/02-specification-language/11579-inductive-params.rst
index 75358ab4ad..28bc8e9592 100644
--- a/doc/changelog/02-specification-language/11579-inductive-params.rst
+++ b/doc/changelog/02-specification-language/11579-inductive-params.rst
@@ -1,4 +1,7 @@
-- **Changed:**
-  Treatment of implicit inductive parameters in inductive declarations is less adhoc.
-  (`#11579 <https://github.com/coq/coq/pull/11579>`_,
-  by Maxime Dénès, Gaëtan Gilbert and Jasper Hugunin).
+- **Fixed:**
+  More robust and expressive treatment of implicit inductive
+  parameters in inductive declarations (`#11579
+  <https://github.com/coq/coq/pull/11579>`_, by Maxime Dénès, Gaëtan
+  Gilbert and Jasper Hugunin; fixes `#7253
+  <https://github.com/coq/coq/pull/7253>`_ and `#11585
+  <https://github.com/coq/coq/pull/11585>`_)
-- 
cgit v1.2.3