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