Feature: compile before require

[elefthei]

Hello and thank you for maintaining VSCoq! This is either a question of "how do I do this" or a feature request. The feature is "Compile before require" as seen in Proof general.

I'd like vscoq to handle Require Foo, by searching in the LoadPath for Foo.v and recompile it with _CoqProject options, before sending the Require Foo to coqtop.

This is obviously something of a preference, not a requirement for everyone. In fact people who care about making their imports faster might want to disable this. However, this works great when teaching Coq to newcomers, because they don't have to deal with .vo files at all this way.

[RalfJung]

Yes I would love to see this! In fact, for big developments, I don't know how to work productively in Coq without a feature like this. I often end up having to do changes than affect many things in many files, so I need help from the IDE to ensure that when I edit some file, all its dependencies have been rebuilt as needed.