Improving e11854569b8 on when to print goals in coqtop mode.
Removing import of Proofview in debugger because its module Goal hides
the import of goal.ml and, afaiu, ocaml does not provide a way to
refer to a shadowed module.
Exporting store of goals so that new_evar in convert, intro, etc. can
propagate it. This allows C-zar to continue to work.

Don't know if it is the best way to do it.
Had forgotten some debugging printer.
Improved tracking of the origin of evars.
Improving evar restriction (this is a risky change, as I remember a
similar optimization broke at some time some ssreflect code; we now
treat the easy case of a let-in to a rel - a pattern common in
pattern-matching compilation -; later on, we shall want to investigate
whether any let-in found to refer to out of scope rels or vars can be
filtered out).
Ensuring that ide_slave and stm receive only .v files from CoqIDE.
In particular, renouncing to original support for existing non .v
files in CoqIDE (hoping it is ok for anyone). Please amend if better
to propose.
Protecting from a List.nth when applying a command, e.g. C-w, on no CoqIDE buffer.