aboutsummaryrefslogtreecommitdiff
path: root/doc/changelog/05-tactic-language/13920-ltac2-ind-api.rst
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).