coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-05-23	Fixing typos - Part 3	JPR

2019-05-21	[loadpath] Factor in common logic for vio/vo file selection.	Emilio Jesus Gallego Arias

2019-05-21	[loadpath] Further cleanup after merge with MlTop.	Emilio Jesus Gallego Arias
	We cleanup a bit the implementation of LoadPath which is not possible as now all the loadpath logic is in the same place. In particular, we remove exceptions in favor a `locate_result` monad. More cleanup should still be possible, in particular `locate_absolute_library` and `locate_qualified_library` should be merged.
2019-05-21	[loadpath] Make loadpath handling self-contained and move to vernac	Emilio Jesus Gallego Arias
	We consolidate loadpath handling as a single `Loadpath` module from parts in `Library` and `Mltop`, placing it at the `vernac` level [as `Mltop`] This idea was first suggested in https://github.com/coq/coq/pull/9808 , and indeed it makes sense as library resolution tends to be business of the upper layers: IDE / build tools. Logic could be pushed upwards, but this is good enough for now. This consolidation has enabled some good and long overdue refactorings, and the module should become self-contained enough as to allow the resolution logic to be shared with `coqdep` in the future. The `Mltop` module only cares now about ML-level modules, and should go away once we rewrite the loader using `findlib` to solve https://github.com/coq/coq/issues/7698 .