aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/02-specification-language/11579-inductive-params.rst
blob: 28bc8e959204b0aa4a22d6bdf65585983095303d (plain)
1
2
3
4
5
6
7
- **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>`_)