aboutsummaryrefslogtreecommitdiff
path: root/vernac/command.ml
AgeCommit message (Expand)Author
2017-03-14[future] Remove unused parameter greedy.Emilio Jesus Gallego Arias
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias