aboutsummaryrefslogtreecommitdiff
path: root/vernac/misctypes.ml
AgeCommit message (Expand)Author
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-07-01[api] Fix wrong deprecation warning (#7915)Emilio Jesus Gallego Arias
2018-06-12[api] Add compatiblity Misctypes module.Emilio Jesus Gallego Arias