[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.

1 files changed, 4 insertions, 2 deletions

diff --git a/library/coqlib.ml b/library/coqlib.ml
index b1e4ef2b00..11d053624c 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -104,8 +104,10 @@ let gen_reference_in_modules locstr dirs s =
 
 let check_required_library d =
   let dir = make_dir d in
-  if Library.library_is_loaded dir then ()
-  else
+  try
+    let _ : Declarations.module_body = Global.lookup_module (ModPath.MPfile dir) in
+    ()
+  with Not_found ->
     let in_current_dir = match Lib.current_mp () with
       | MPfile dp -> DirPath.equal dir dp
       | _ -> false