[library] Move library to vernac

This is step 1 on removing library state from the lower layers.

Here we move library loading to the vernacular layer; few things
depend on it:

- printers: we add a parameter for those needing to access on-disk data,

- coqlib: indeed a few tactics do try to check that a particular
  library is loaded; this is a tricky part. I've replaced that for a
  module name check, but indeed this is fully equivalent due to
  side-effects of `Require`. We may want to think what to do here.

A few other minor code movements were needed, but there are
self-explanatory.

0 files changed, 0 insertions, 0 deletions