aboutsummaryrefslogtreecommitdiff
path: root/vernac/loadpath.mli
AgeCommit message (Expand)Author
2019-05-23Fixing typos - Part 3JPR
2019-05-21[loadpath] Further cleanup after merge with MlTop.Emilio Jesus Gallego Arias
2019-05-21[loadpath] Make loadpath handling self-contained and move to vernacEmilio Jesus Gallego Arias