aboutsummaryrefslogtreecommitdiff
path: root/vernac/comSearch.ml
AgeCommit message (Expand)Author
2020-05-15Deprecate SearchHead.Théo Zimmermann
2020-05-15Moving interpretation of Search commands to their own file: comSearch.ml.Hugo Herbelin