blob: 7e34c4a0ff943a79fe4710c2647329bc5caca3d6 (
plain)
1
2
3
4
5
|
- **Changed:** The warning when using :cmd:`Require` inside a section
moved from the ``deprecated`` category to the ``fragile`` category,
because there is no plan to remove the functionality at this time.
(`#11972 <https://github.com/coq/coq/pull/11972>`_, by Gaëtan
Gilbert).
|
