Removed the concept of "weirdness" from the Coq Makefile generator

As all projects have an abstract load path entry for the Coq standard
library, the generator has always considered them to be weird, so there's
no reason to keep the simple case
Made the PIDE editor render Coq processing annotations

This is really naïve at the moment -- annotations are always discarded
instead of being updated, and all annotations are always replaced,
regardless of how big the document change was -- but it's a start
Use the Protocol.Status object to decide whether a command is finished
Don't print PIDE goal messages to the console
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
Bumped the version numbers to 0.4.6.2 and added a changelog entry