aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/misctypes.ml
Commit message (Collapse)AuthorAge
* [api] Fix wrong deprecation warning (#7915)Gravatar Emilio Jesus Gallego Arias2018-07-01
| | | | | | | Fixes: #7915. Due to a change in the original misctypes removal PR, the deprecation notice went out of sync.
* [api] Add compatiblity Misctypes module.Gravatar Emilio Jesus Gallego Arias2018-06-12
To be removed in 8.10.