blob: 32499957be11c1224a9f4bbb954b2017c5965aab (
plain)
1
2
3
4
5
|
- **Added:**
Added the Ltac2 API `Ltac2.Ind` for manipulating inductive types
(`#13920 <https://github.com/coq/coq/pull/13920>`_,
fixes `#10095 <https://github.com/coq/coq/issues/10095>`_,
by Pierre-Marie Pédrot).
|