aboutsummaryrefslogtreecommitdiff
path: root/vernac/comSearch.ml
AgeCommit message (Expand)Author
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2021-01-25Remove the SearchHead commandJim Fehrle
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-04Typing patterns and using type constraints in Search.Hugo Herbelin
2020-05-15Deprecate SearchHead.Théo Zimmermann
2020-05-15Moving interpretation of Search commands to their own file: comSearch.ml.Hugo Herbelin