The Coq builder should resolve Load and Require sentences in the same way

This was already (almost) the case -- because of a bug. A conditional was
never updated to reflect changes made to DependencyTracker, the result of
which was that the code accidentally did the right thing most of the time!
Now it does the right thing for the right reasons...
The Coq project builder should track where identifiers come from

This will make it possible to provide more helpful error messages when
dependency resolution fails
Create multiple error markers when dependency resolution fails

This commit also adds location information to each of these error markers
Report the offset of an error as its location where necessary

Obviously the offset is not nearly as helpful as a line number, but that's
more expensive to compute, and the offset is better than nothing
Made the Coq builder's dependency error messages mimic those of Coq