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>`_)
|