Merge PR #10562: [library] Move library to vernac

Reviewed-by: maximedenes

12 files changed, 116 insertions, 93 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
diff --git a/library/library.mllib b/library/library.mllib
index 3b75438ccd..c34d8911e8 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -6,7 +6,6 @@ Nametab
 Global
 Lib
 Declaremods
-Library
 States
 Kindops
 Goptions
diff --git a/library/states.ml b/library/states.ml
index a73f16957d..0be153d96a 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Util
-open System
 
 type state = Lib.frozen * Summary.frozen
 
@@ -25,13 +24,6 @@ let unfreeze (fl,fs) =
   Lib.unfreeze fl;
   Summary.unfreeze_summaries fs
 
-let extern_state s =
-  System.extern_state Coq_config.state_magic_number s (freeze ~marshallable:true)
-
-let intern_state s =
-  unfreeze (with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
-  Library.overwrite_library_filenames s
-
 (* Rollback. *)
 
 let with_state_protection f x =
diff --git a/library/states.mli b/library/states.mli
index c4f3eae49d..4870f48fc3 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -15,9 +15,6 @@
   freezing the states of both [Lib] and [Summary]. We provide functions
   to write and restore state to and from a given file. *)
 
-val intern_state : string -> unit
-val extern_state : string -> unit
-
 type state
 val freeze : marshallable:bool -> state
 val unfreeze : state -> unit
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b7fefca22b..fb0b1eca8d 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -35,14 +35,14 @@ module NamedDecl = Context.Named.Declaration
 
 type object_pr = {
   print_inductive           : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
-  print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t;
   print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
   print_modtype             : ModPath.t -> Pp.t;
   print_named_decl          : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
-  print_library_entry       : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option;
-  print_context             : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
+  print_library_entry       : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option;
+  print_context             : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
   print_typed_value_in_env  : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
   print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
 }
@@ -560,10 +560,10 @@ let print_instance sigma cb =
     let inst = Univ.make_abstract_instance univs in
     pr_universe_instance sigma inst
   else mt()
-				
-let print_constant with_values sep sp udecl =
+
+let print_constant indirect_accessor with_values sep sp udecl =
   let cb = Global.lookup_constant sp in
-  let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in
+  let val_0 = Global.body_of_constant_body indirect_accessor cb in
   let typ = cb.const_type in
   let univs =
     let open Univ in
@@ -571,7 +571,7 @@ let print_constant with_values sep sp udecl =
     match cb.const_body with
     | Undef _ | Def _ | Primitive _ -> cb.const_universes
     | OpaqueDef o ->
-      let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in
+      let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in
       match cb.const_universes with
       | Monomorphic ctx ->
         Monomorphic (ContextSet.union body_uctxs ctx)
@@ -601,8 +601,8 @@ let print_constant with_values sep sp udecl =
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
         Printer.pr_universes sigma univs ?priv)
 
-let gallina_print_constant_with_infos sp udecl =
-  print_constant true " = " sp udecl ++
+let gallina_print_constant_with_infos indirect_accessor sp udecl =
+  print_constant indirect_accessor true " = " sp udecl ++
   with_line_skip (print_name_infos (GlobRef.ConstRef sp))
 
 let gallina_print_syntactic_def env kn =
@@ -618,7 +618,7 @@ let gallina_print_syntactic_def env kn =
      Constrextern.without_specific_symbols
        [Notation.SynDefRule kn] (pr_glob_constr_env env) c)
 
-let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
+let gallina_print_leaf_entry indirect_accessor env sigma with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : " in
   match lobj with
   | AtomicObject o ->
@@ -629,7 +629,7 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
              constraints *)
           (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None)
       | (_,"CONSTANT") ->
-          Some (print_constant with_values sep (Constant.make1 kn) None)
+          Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None)
       | (_,"INDUCTIVE") ->
           Some (gallina_print_inductive (MutInd.make1 kn) None)
       | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
@@ -645,24 +645,24 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
           Some (print_modtype (MPdot (mp,l)))
   | _ -> None
 
-let gallina_print_library_entry env sigma with_values ent =
+let gallina_print_library_entry indirect_accessor env sigma with_values ent =
   let pr_name (sp,_) = Id.print (basename sp) in
   match ent with
     | (oname,Lib.Leaf lobj) ->
-        gallina_print_leaf_entry env sigma with_values (oname,lobj)
+      gallina_print_leaf_entry indirect_accessor env sigma with_values (oname,lobj)
     | (oname,Lib.OpenedSection (dir,_)) ->
-        Some (str " >>>>>>> Section " ++ pr_name oname)
+      Some (str " >>>>>>> Section " ++ pr_name oname)
     | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) ->
-        Some (str " >>>>>>> Library " ++ DirPath.print obj_dir)
+      Some (str " >>>>>>> Library " ++ DirPath.print obj_dir)
     | (oname,Lib.OpenedModule _) ->
-	Some (str " >>>>>>> Module " ++ pr_name oname)
+      Some (str " >>>>>>> Module " ++ pr_name oname)
 
-let gallina_print_context env sigma with_values =
+let gallina_print_context indirect_accessor env sigma with_values =
   let rec prec n = function
     | h::rest when Option.is_empty n || Option.get n > 0 ->
-        (match gallina_print_library_entry env sigma with_values h with
-	  | None -> prec n rest
-	  | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ())
+      (match gallina_print_library_entry indirect_accessor env sigma with_values h with
+       | None -> prec n rest
+       | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ())
     | _ -> mt ()
   in
   prec
@@ -720,10 +720,10 @@ let print_safe_judgment env sigma j =
 (*********************)
 (* *)
 
-let print_full_context env sigma = print_context env sigma true None (Lib.contents ())
-let print_full_context_typ env sigma = print_context env sigma false None (Lib.contents ())
+let print_full_context indirect_accessor env sigma = print_context indirect_accessor env sigma true None (Lib.contents ())
+let print_full_context_typ indirect_accessor env sigma = print_context indirect_accessor env sigma false None (Lib.contents ())
 
-let print_full_pure_context env sigma =
+let print_full_pure_context ~library_accessor env sigma =
   let rec prec = function
   | ((_,kn),Lib.Leaf AtomicObject lobj)::rest ->
       let pp = match object_tag lobj with
@@ -739,8 +739,8 @@ let print_full_pure_context env sigma =
 	      | OpaqueDef lc ->
 		str "Theorem " ++ print_basename con ++ cut () ++
                 str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++
-                str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc))
-	      | Def c ->
+                str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc))
+              | Def c ->
 		str "Definition " ++ print_basename con ++ cut () ++
                 str "  : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++
                 pr_lconstr_env env sigma (Mod_subst.force_constr c)
@@ -787,11 +787,11 @@ let read_sec_context qid =
   let cxt = Lib.contents () in
   List.rev (get_cxt [] cxt)
 
-let print_sec_context env sigma sec =
-  print_context env sigma true None (read_sec_context sec)
+let print_sec_context indirect_accessor env sigma sec =
+  print_context indirect_accessor env sigma true None (read_sec_context sec)
 
-let print_sec_context_typ env sigma sec =
-  print_context env sigma false None (read_sec_context sec)
+let print_sec_context_typ indirect_accessor env sigma sec =
+  print_context indirect_accessor env sigma false None (read_sec_context sec)
 
 let maybe_error_reject_univ_decl na udecl =
   let open GlobRef in
@@ -801,11 +801,11 @@ let maybe_error_reject_univ_decl na udecl =
     (* TODO Print na somehow *)
     user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.")
 
-let print_any_name env sigma na udecl =
+let print_any_name indirect_accessor env sigma na udecl =
   maybe_error_reject_univ_decl na udecl;
   let open GlobRef in
   match na with
-  | Term (ConstRef sp) -> print_constant_with_infos sp udecl
+  | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor sp udecl
   | Term (IndRef (sp,_)) -> print_inductive sp udecl
   | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl
   | Term (VarRef sp) -> print_section_variable env sigma sp
@@ -824,34 +824,34 @@ let print_any_name env sigma na udecl =
     user_err
       ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
-let print_name env sigma na udecl =
+let print_name indirect_accessor env sigma na udecl =
   match na with
   | {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
-      print_any_name env sigma
-        (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+    print_any_name indirect_accessor env sigma
+      (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc))
-        udecl
+      udecl
   | {loc; v=Constrexpr.AN ref} ->
-      print_any_name env sigma (locate_any_name ref) udecl
+    print_any_name indirect_accessor env sigma (locate_any_name ref) udecl
 
-let print_opaque_name env sigma qid =
+let print_opaque_name indirect_accessor env sigma qid =
   let open GlobRef in
   match Nametab.global qid with
     | ConstRef cst ->
-	let cb = Global.lookup_constant cst in
-        if Declareops.constant_has_body cb then
-          print_constant_with_infos cst None
-        else
-	  user_err Pp.(str "Not a defined constant.")
+      let cb = Global.lookup_constant cst in
+      if Declareops.constant_has_body cb then
+        print_constant_with_infos indirect_accessor cst None
+      else
+        user_err Pp.(str "Not a defined constant.")
     | IndRef (sp,_) ->
-        print_inductive sp None
+      print_inductive sp None
     | ConstructRef cstr as gr ->
-        let ty, ctx = Typeops.type_of_global_in_context env gr in
-	let ty = EConstr.of_constr ty in
-        let open EConstr in
-        print_typed_value_in_env env sigma (mkConstruct cstr, ty)
+      let ty, ctx = Typeops.type_of_global_in_context env gr in
+      let ty = EConstr.of_constr ty in
+      let open EConstr in
+      print_typed_value_in_env env sigma (mkConstruct cstr, ty)
     | VarRef id ->
-        env |> lookup_named id |> print_named_decl env sigma
+      env |> lookup_named id |> print_named_decl env sigma
 
 let print_about_any ?loc env sigma k udecl =
   maybe_error_reject_univ_decl k udecl;
@@ -888,9 +888,8 @@ let print_about env sigma na udecl =
       print_about_any ?loc env sigma (locate_any_name ref) udecl
 
 (* for debug *)
-let inspect env sigma depth =
-  print_context env sigma false (Some depth) (Lib.contents ())
-
+let inspect indirect_accessor env sigma depth =
+  print_context indirect_accessor env sigma false (Some depth) (Lib.contents ())
 
 (*************************************************************************)
 (* Pretty-printing functions coming from classops.ml                     *)
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 7485f4bd19..4299bcc880 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -18,22 +18,41 @@ open Libnames
 val assumptions_for_print : Name.t list -> Termops.names_context
 
 val print_closed_sections : bool ref
-val print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t
-val print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option
-val print_full_context : env -> Evd.evar_map -> Pp.t
-val print_full_context_typ : env -> Evd.evar_map -> Pp.t
-val print_full_pure_context : env -> Evd.evar_map -> Pp.t
-val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t
-val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t
+val print_context
+  : Opaqueproof.indirect_accessor
+  -> env -> Evd.evar_map
+  -> bool -> int option -> Lib.library_segment -> Pp.t
+val print_library_entry
+  : Opaqueproof.indirect_accessor
+  -> env -> Evd.evar_map
+  -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option
+val print_full_context
+ : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t
+val print_full_context_typ
+  : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t
+
+val print_full_pure_context
+  : library_accessor:Opaqueproof.indirect_accessor
+  -> env
+  -> Evd.evar_map
+  -> Pp.t
+
+val print_sec_context
+  : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t
+val print_sec_context_typ
+  : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t
 val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t
 val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t
 val print_eval :
   reduction_function -> env -> Evd.evar_map ->
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
-val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
-  UnivNames.univ_name_list option -> Pp.t
-val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t
+val print_name
+  : Opaqueproof.indirect_accessor
+  -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation
+  -> UnivNames.univ_name_list option -> Pp.t
+val print_opaque_name
+  : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t
 val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation ->
   UnivNames.univ_name_list option -> Pp.t
 val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t
@@ -50,7 +69,7 @@ val print_typeclasses : unit -> Pp.t
 val print_instances : GlobRef.t -> Pp.t
 val print_all_instances : unit -> Pp.t
 
-val inspect : env -> Evd.evar_map -> int -> Pp.t
+val inspect : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> int -> Pp.t
 
 (** {5 Locate} *)
 
@@ -83,14 +102,14 @@ val print_located_other : string -> qualid -> Pp.t
 
 type object_pr = {
   print_inductive           : MutInd.t -> UnivNames.univ_name_list option -> Pp.t;
-  print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t;
   print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
   print_modtype             : ModPath.t -> Pp.t;
   print_named_decl          : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t;
-  print_library_entry       : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option;
-  print_context             : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
+  print_library_entry       : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option;
+  print_context             : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t;
   print_typed_value_in_env  : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
   print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
 }
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index 019577ac85..7658ad68a5 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -11,7 +11,7 @@
 let outputstate opts =
   Option.iter (fun ostate_file ->
     let fname = CUnix.make_suffix ostate_file ".coq" in
-    States.extern_state fname) opts.Coqcargs.outputstate
+    Library.extern_state fname) opts.Coqcargs.outputstate
 
 let coqc_init _copts ~opts =
   Flags.quiet := true;
@@ -53,7 +53,8 @@ let coqc_main copts ~opts =
 
   if opts.Coqargs.post.Coqargs.output_context then begin
     let sigma, env = let e = Global.env () in Evd.from_env e, e in
-    Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
+    let library_accessor = Library.indirect_accessor in
+    Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~library_accessor env) sigma) ++ fnl ())
   end;
   CProfile.print_profile ()
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f09d202edf..33a95e7b30 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -87,7 +87,7 @@ let set_options = List.iter set_option
 let inputstate opts =
   Option.iter (fun istate_file ->
     let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in
-    States.intern_state fname) opts.inputstate
+    Library.intern_state fname) opts.inputstate
 
 (******************************************************************************)
 (* Fatal Errors                                                               *)
diff --git a/library/library.ml b/vernac/library.ml
index 0faef7bf84..e91cb965f5 100644
--- a/library/library.ml
+++ b/vernac/library.ml
@@ -474,10 +474,10 @@ let require_library_from_dirpath ~lib_resolver modrefl export =
     if Lib.is_module_or_modtype () then
       begin
         warn_require_in_module ();
-	add_anonymous_leaf (in_require (needed,modrefl,None));
-	Option.iter (fun exp ->
-	  add_anonymous_leaf (in_import_library (modrefl,exp)))
-	  export
+        add_anonymous_leaf (in_require (needed,modrefl,None));
+        Option.iter (fun exp ->
+          add_anonymous_leaf (in_import_library (modrefl,exp)))
+          export
       end
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
@@ -547,7 +547,7 @@ let current_deps () =
 let current_reexports () = !libraries_exports_list
 
 let error_recursively_dependent_library dir =
-  user_err 
+  user_err
     (strbrk "Unable to use logical name " ++ DirPath.print dir ++
      strbrk " to save current library because" ++
      strbrk " it already depends on a library of this name.")
@@ -640,3 +640,12 @@ let get_used_load_paths () =
        StringSet.empty !libraries_loaded_list)
 
 let _ = Nativelib.get_load_paths := get_used_load_paths
+
+(* These commands may not be very safe due to ML-side plugin loading
+   etc... use at your own risk *)
+let extern_state s =
+  System.extern_state Coq_config.state_magic_number s (States.freeze ~marshallable:true)
+
+let intern_state s =
+  States.unfreeze (System.with_magic_number_check (System.intern_state Coq_config.state_magic_number) s);
+  overwrite_library_filenames s
diff --git a/library/library.mli b/vernac/library.mli
index bb6c42e393..973b369226 100644
--- a/library/library.mli
+++ b/vernac/library.mli
@@ -75,3 +75,7 @@ val native_name_from_filename : string -> string
 
 (** {6 Opaque accessors} *)
 val indirect_accessor : Opaqueproof.indirect_accessor
+
+(** Low-level state overwriting, not very safe *)
+val intern_state : string -> unit
+val extern_state : string -> unit
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 20de6b4ff2..cd13f83e96 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -16,6 +16,7 @@ DeclareDef
 DeclareObl
 Canonical
 RecLemmas
+Library
 Lemmas
 Class
 Auto_ind_decl
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6180ab0821..90b7610750 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1179,11 +1179,11 @@ let vernac_chdir = function
 
 let vernac_write_state file =
   let file = CUnix.make_suffix file ".coq" in
-  States.extern_state file
+  Library.extern_state file
 
 let vernac_restore_state file =
   let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
-  States.intern_state file
+  Library.intern_state file
 
 (************)
 (* Commands *)
@@ -1972,9 +1972,9 @@ let vernac_print ~pstate ~atts =
   function
   | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ()))
   | PrintTables -> print_tables ()
-  | PrintFullContext-> print_full_context_typ env sigma
-  | PrintSectionContext qid -> print_sec_context_typ env sigma qid
-  | PrintInspect n -> inspect env sigma n
+  | PrintFullContext-> print_full_context_typ Library.indirect_accessor env sigma
+  | PrintSectionContext qid -> print_sec_context_typ Library.indirect_accessor env sigma qid
+  | PrintInspect n -> inspect Library.indirect_accessor env sigma n
   | PrintGrammar ent -> Metasyntax.pr_grammar ent
   | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent
   | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
@@ -1987,7 +1987,7 @@ let vernac_print ~pstate ~atts =
   | PrintDebugGC -> Mltop.print_gc ()
   | PrintName (qid,udecl) ->
     dump_global qid;
-    print_name env sigma qid udecl
+    print_name Library.indirect_accessor env sigma qid udecl
   | PrintGraph -> Prettyp.print_graph ()
   | PrintClasses -> Prettyp.print_classes()
   | PrintTypeClasses -> Prettyp.print_typeclasses()