aboutsummaryrefslogtreecommitdiff
path: root/vernac/pvernac.mli
AgeCommit message (Expand)Author
2018-05-30Move interning the [hint_pattern] outside the Typeclasses hooks.Gaƫtan Gilbert
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias