aboutsummaryrefslogtreecommitdiff
path: root/vernac/comSearch.ml
AgeCommit message (Collapse)Author
2020-05-15Deprecate SearchHead.Théo Zimmermann
The main use case of SearchHead is now handled by headconcl: The secondary use case was redundant with SearchPattern.
2020-05-15Moving interpretation of Search commands to their own file: comSearch.ml.Hugo Herbelin