[printing] Deprecate all printing functions accessing the global proof.

We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.

We also adapt most of the code, making more explicit where the
printing environment is coming from.

An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.

7 files changed, 137 insertions, 109 deletions

diff --git a/printing/pputils.ml b/printing/pputils.ml
index 3cc7a3e6b..12d5338ad 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -103,6 +103,9 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
   | CbvNative o ->
     keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
 
+let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
+  pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
+
 let pr_or_by_notation f = function
   | AN v -> f v
   | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 1f4fa1390..f7f586b77 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -21,8 +21,16 @@ val pr_with_occurrences :
 
 val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
 val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
+
 val pr_red_expr :
   ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
+  (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t
+
+val pr_red_expr_env : Environ.env -> Evd.evar_map ->
+  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+  ('b -> Pp.t) *
+  (Environ.env -> Evd.evar_map -> 'c -> Pp.t) ->
   (string -> Pp.t) ->
   ('a,'b,'c) red_expr_gen -> Pp.t
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index acbd2d5d2..e2d23ce7b 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -35,13 +35,13 @@ module NamedDecl = Context.Named.Declaration
 type object_pr = {
   print_inductive           : MutInd.t -> Pp.t;
   print_constant_with_infos : Constant.t -> Pp.t;
-  print_section_variable    : variable -> Pp.t;
-  print_syntactic_def       : KerName.t -> 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          : Context.Named.Declaration.t -> Pp.t;
-  print_library_entry       : bool -> (object_name * Lib.node) -> Pp.t option;
-  print_context             : bool -> int option -> Lib.library_segment -> Pp.t;
+  print_named_decl          : env -> Evd.evar_map -> Context.Named.Declaration.t -> 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_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;
 }
@@ -487,25 +487,25 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) =
    the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
    synthesizes the type nat of the abstraction on u *)
 
-let print_named_def name body typ =
-  let pbody = pr_lconstr body in
-  let ptyp = pr_ltype typ in
+let print_named_def env sigma name body typ =
+  let pbody = pr_lconstr_env env sigma body in
+  let ptyp = pr_ltype_env env sigma typ in
   let pbody = if isCast body then surround pbody else pbody in
   (str "*** [" ++ str name ++ str " " ++
      hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++
 	      str ":" ++ brk (1,2) ++ ptyp) ++
 	   str "]")
 
-let print_named_assum name typ =
-  str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]"
+let print_named_assum env sigma name typ =
+  str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]"
 
-let gallina_print_named_decl =
+let gallina_print_named_decl env sigma =
   let open Context.Named.Declaration in
   function
   | LocalAssum (id, typ) ->
-     print_named_assum (Id.to_string id) typ
+     print_named_assum env sigma (Id.to_string id) typ
   | LocalDef (id, body, typ) ->
-     print_named_def (Id.to_string id) body typ
+     print_named_def env sigma (Id.to_string id) body typ
 
 let assumptions_for_print lna =
   List.fold_right (fun na env -> add_name na env) lna empty_names_context
@@ -524,11 +524,11 @@ let gallina_print_inductive sp =
      print_inductive_implicit_args sp mipv @
      print_inductive_argument_scopes sp mipv)
 
-let print_named_decl id =
-  gallina_print_named_decl (Global.lookup_named id) ++ fnl ()
+let print_named_decl env sigma id =
+  gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl ()
 
-let gallina_print_section_variable id =
-  print_named_decl id ++
+let gallina_print_section_variable env sigma id =
+  print_named_decl env sigma id ++
   with_line_skip (print_name_infos (VarRef id))
 
 let print_body env evd = function
@@ -601,7 +601,7 @@ let gallina_print_constant_with_infos sp =
   print_constant true " = " sp ++
   with_line_skip (print_name_infos (ConstRef sp))
 
-let gallina_print_syntactic_def kn =
+let gallina_print_syntactic_def env kn =
   let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn
   and (vars,a) = Syntax_def.search_syntactic_definition kn in
   let c = Notation_ops.glob_constr_of_notation_constr a in
@@ -612,16 +612,16 @@ let gallina_print_syntactic_def kn =
         spc () ++ str ":=") ++
      spc () ++
      Constrextern.without_specific_symbols
-       [Notation.SynDefRule kn] pr_glob_constr c)
+       [Notation.SynDefRule kn] (pr_glob_constr_env env) c)
 
-let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
+let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
   let sep = if with_values then " = " else " : "
   and tag = object_tag lobj in
     match (oname,tag) with
       | (_,"VARIABLE") ->
 	  (* Outside sections, VARIABLES still exist but only with universes
              constraints *)
-	  (try Some(print_named_decl (basename sp)) with Not_found -> None)
+          (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None)
       | (_,"CONSTANT") ->
 	  Some (print_constant with_values sep (Constant.make1 kn))
       | (_,"INDUCTIVE") ->
@@ -637,11 +637,11 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) =
       (* To deal with forgotten cases... *)
       | (_,s) -> None
 
-let gallina_print_library_entry with_values ent =
+let gallina_print_library_entry 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 with_values (oname,lobj)
+        gallina_print_leaf_entry env sigma with_values (oname,lobj)
     | (oname,Lib.OpenedSection (dir,_)) ->
         Some (str " >>>>>>> Section " ++ pr_name oname)
     | (oname,Lib.ClosedSection _) ->
@@ -653,10 +653,10 @@ let gallina_print_library_entry with_values ent =
     | (oname,Lib.ClosedModule _) ->
         Some (str " >>>>>>> Closed Module " ++ pr_name oname)
 
-let gallina_print_context with_values =
+let gallina_print_context 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 with_values h with
+        (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 ())
     | _ -> mt ()
@@ -718,10 +718,10 @@ let print_safe_judgment env sigma j =
 (*********************)
 (* *)
 
-let print_full_context () = print_context true None (Lib.contents ())
-let print_full_context_typ () = print_context false None (Lib.contents ())
+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_pure_context () =
+let print_full_pure_context env sigma =
   let rec prec = function
   | ((_,kn),Lib.Leaf lobj)::rest ->
       let pp = match object_tag lobj with
@@ -733,15 +733,15 @@ let print_full_pure_context () =
 	    match cb.const_body with
 	      | Undef _ ->
 		str "Parameter " ++
-		print_basename con ++ str " : " ++ cut () ++ pr_ltype typ
+                print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ
 	      | OpaqueDef lc ->
 		str "Theorem " ++ print_basename con ++ cut () ++
-		str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
-		str "Proof " ++ pr_lconstr (Opaqueproof.force_proof (Global.opaque_tables ()) lc)
+                str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++
+                str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof (Global.opaque_tables ()) lc)
 	      | Def c ->
 		str "Definition " ++ print_basename con ++ cut () ++
-		str "  : " ++ pr_ltype typ ++ cut () ++ str " := " ++
-		pr_lconstr (Mod_subst.force_constr c))
+                str "  : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++
+                pr_lconstr_env env sigma (Mod_subst.force_constr c))
           ++ str "." ++ fnl () ++ fnl ()
       | "INDUCTIVE" ->
 	  let mind = Global.mind_of_delta_kn kn in
@@ -787,18 +787,18 @@ let read_sec_context r =
   let cxt = Lib.contents () in
   List.rev (get_cxt [] cxt)
 
-let print_sec_context sec =
-  print_context true None (read_sec_context sec)
+let print_sec_context env sigma sec =
+  print_context env sigma true None (read_sec_context sec)
 
-let print_sec_context_typ sec =
-  print_context false 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_any_name = function
+let print_any_name env sigma = function
   | Term (ConstRef sp) -> print_constant_with_infos sp
   | Term (IndRef (sp,_)) -> print_inductive sp
   | Term (ConstructRef ((sp,_),_)) -> print_inductive sp
-  | Term (VarRef sp) -> print_section_variable sp
-  | Syntactic kn -> print_syntactic_def kn
+  | Term (VarRef sp) -> print_section_variable env sigma sp
+  | Syntactic kn -> print_syntactic_def env kn
   | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
   | Dir _ -> mt ()
   | ModuleType mp -> print_modtype mp
@@ -807,22 +807,21 @@ let print_any_name = function
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in
     if not (DirPath.is_empty dir) then raise Not_found;
-    str |> Global.lookup_named |> print_named_decl
+    str |> Global.lookup_named |> print_named_decl env sigma
 
   with Not_found ->
     user_err
       ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
-let print_name = function
+let print_name env sigma = function
   | ByNotation (loc,(ntn,sc)) ->
-      print_any_name
+      print_any_name env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc))
   | AN ref ->
-      print_any_name (locate_any_name ref)
+      print_any_name env sigma (locate_any_name ref)
 
-let print_opaque_name qid =
-  let env = Global.env () in
+let print_opaque_name env sigma qid =
   match Nametab.global qid with
     | ConstRef cst ->
 	let cb = Global.lookup_constant cst in
@@ -840,9 +839,9 @@ let print_opaque_name qid =
         let open EConstr in
 	print_typed_value (mkConstruct cstr, ty)
     | VarRef id ->
-        env |> lookup_named id |> print_named_decl
+        env |> lookup_named id |> print_named_decl env sigma
 
-let print_about_any ?loc k =
+let print_about_any ?loc env sigma k =
   match k with
   | Term ref ->
     let rb = Reductionops.ReductionBehaviour.print ref in
@@ -858,23 +857,23 @@ let print_about_any ?loc k =
     | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref
     | _ -> () in
       v 0 (
-      print_syntactic_def kn ++ fnl () ++
+      print_syntactic_def env kn ++ fnl () ++
       hov 0 (str "Expands to: " ++ pr_located_qualid k))
   | Dir _ | ModuleType _ | Undefined _ ->
       hov 0 (pr_located_qualid k)
   | Other (obj, info) -> hov 0 (info.about obj)
 
-let print_about = function
+let print_about env sigma = function
   | ByNotation (loc,(ntn,sc)) ->
-      print_about_any ?loc
+      print_about_any ?loc env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc))
   | AN ref ->
-      print_about_any ?loc:(loc_of_reference ref) (locate_any_name ref)
+      print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref)
 
 (* for debug *)
-let inspect depth =
-  print_context false (Some depth) (Lib.contents ())
+let inspect env sigma depth =
+  print_context env sigma false (Some depth) (Lib.contents ())
 
 
 (*************************************************************************)
@@ -882,18 +881,20 @@ let inspect depth =
 
 open Classops
 
-let print_coercion_value v = pr_lconstr (get_coercion_value v)
+let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v)
 
 let print_class i =
   let cl,_ = class_info_from_index i in
   pr_class cl
 
 let print_path ((i,j),p) =
+  let sigma, env = Pfedit.get_current_context () in
   hov 2 (
-    str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++
+    str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++
     str"] : ") ++
   print_class i ++ str" >-> " ++ print_class j
 
+(* XXX: This is suspicious!!! *)
 let _ = Classops.install_path_printer print_path
 
 let print_graph () =
@@ -902,8 +903,8 @@ let print_graph () =
 let print_classes () =
   pr_sequence pr_class (classes())
 
-let print_coercions () =
-  pr_sequence print_coercion_value (coercions())
+let print_coercions env sigma =
+  pr_sequence (print_coercion_value env sigma) (coercions())
 
 let index_of_class cl =
   try
@@ -925,11 +926,11 @@ let print_path_between cls clt =
   in
   print_path ((i,j),p)
 
-let print_canonical_projections () =
+let print_canonical_projections env sigma =
   prlist_with_sep fnl
     (fun ((r1,r2),o) -> pr_cs_pattern r2 ++
     str " <- " ++
-    pr_global r1 ++ str " ( " ++ pr_lconstr o.o_DEF ++ str " )")
+    pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )")
     (canonical_projections ())
 
 (*************************************************************************)
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 31fd766ea..89099a043 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -18,37 +18,37 @@ open Misctypes
 val assumptions_for_print : Name.t list -> Termops.names_context
 
 val print_closed_sections : bool ref
-val print_context : bool -> int option -> Lib.library_segment -> Pp.t
-val print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option
-val print_full_context : unit -> Pp.t
-val print_full_context_typ : unit -> Pp.t
-val print_full_pure_context : unit -> Pp.t
-val print_sec_context : reference -> Pp.t
-val print_sec_context_typ : reference -> Pp.t
+val print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t
+val print_library_entry : env -> Evd.evar_map -> bool -> (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 -> reference -> Pp.t
+val print_sec_context_typ : env -> Evd.evar_map -> reference -> 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 : reference or_by_notation -> Pp.t
-val print_opaque_name : reference -> Pp.t
-val print_about : reference or_by_notation -> Pp.t
+val print_name : env -> Evd.evar_map -> reference or_by_notation -> Pp.t
+val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
+val print_about : env -> Evd.evar_map -> reference or_by_notation -> Pp.t
 val print_impargs : reference or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
 val print_graph : unit -> Pp.t
 val print_classes : unit -> Pp.t
-val print_coercions : unit -> Pp.t
+val print_coercions : env -> Evd.evar_map -> Pp.t
 val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t
-val print_canonical_projections : unit -> Pp.t
+val print_canonical_projections : env -> Evd.evar_map -> Pp.t
 
 (** Pretty-printing functions for type classes and instances *)
 val print_typeclasses : unit -> Pp.t
 val print_instances : global_reference -> Pp.t
 val print_all_instances : unit -> Pp.t
 
-val inspect : int -> Pp.t
+val inspect : env -> Evd.evar_map -> int -> Pp.t
 
 (** {5 Locate} *)
 
@@ -82,15 +82,15 @@ val print_located_other : string -> reference -> Pp.t
 type object_pr = {
   print_inductive           : MutInd.t -> Pp.t;
   print_constant_with_infos : Constant.t -> Pp.t;
-  print_section_variable    : variable -> Pp.t;
-  print_syntactic_def       : KerName.t -> 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          : Context.Named.Declaration.t -> Pp.t;
-  print_library_entry       : bool -> (object_name * Lib.node) -> Pp.t option;
-  print_context             : bool -> int option -> Lib.library_segment -> Pp.t;
+  print_named_decl          : env -> Evd.evar_map -> Context.Named.Declaration.t -> 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_typed_value_in_env  : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t;
-  print_eval                : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
+  print_eval                : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t;
 }
 
 val set_object_pr : object_pr -> unit
diff --git a/printing/printer.ml b/printing/printer.ml
index ba31b72d6..377a6b4e1 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -26,9 +26,6 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 module CompactedDecl = Context.Compacted.Declaration
 
-let get_current_context () =
-  Pfedit.get_current_context ()
-
 let enable_unfocused_goal_printing = ref false
 let enable_goal_tags_printing = ref false
 let enable_goal_names_printing = ref false
@@ -104,10 +101,10 @@ let pr_econstr_env env sigma c = pr_econstr_core false env sigma c
 
 (* NB do not remove the eta-redexes! Global.env() has side-effects... *)
 let pr_lconstr t =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   pr_lconstr_env env sigma t
 let pr_constr t =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   pr_constr_env env sigma t
 
 let pr_open_lconstr (_,c) = pr_lconstr c
@@ -127,10 +124,10 @@ let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env
 let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env
 
 let pr_constr_under_binders c =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   pr_constr_under_binders_env env sigma c
 let pr_lconstr_under_binders c =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   pr_lconstr_under_binders_env env sigma c
 
 let pr_etype_core goal_concl_style env sigma t =
@@ -142,10 +139,10 @@ let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr
 let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c)
 
 let pr_ltype t =
-    let (sigma, env) = get_current_context () in
+    let (sigma, env) = Pfedit.get_current_context () in
     pr_ltype_env env sigma t
 let pr_type t =
-    let (sigma, env) = get_current_context () in
+    let (sigma, env) = Pfedit.get_current_context () in
     pr_type_env env sigma t
 
 let pr_etype_env env sigma c = pr_etype_core false env sigma c
@@ -156,7 +153,7 @@ let pr_ljudge_env env sigma j =
   (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)
 
 let pr_ljudge j =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   pr_ljudge_env env sigma j
 
 let pr_lglob_constr_env env c =
@@ -165,10 +162,10 @@ let pr_glob_constr_env env c =
   pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c)
 
 let pr_lglob_constr c =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   pr_lglob_constr_env env c
 let pr_glob_constr c =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   pr_glob_constr_env env c
 
 let pr_closed_glob_n_env env sigma n c =
@@ -176,7 +173,7 @@ let pr_closed_glob_n_env env sigma n c =
 let pr_closed_glob_env env sigma c =
   pr_constr_expr (extern_closed_glob false env sigma c)
 let pr_closed_glob c =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   pr_closed_glob_env env sigma c
 
 let pr_lconstr_pattern_env env sigma c =
@@ -188,10 +185,10 @@ let pr_cases_pattern t =
   pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t)
 
 let pr_lconstr_pattern t =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   pr_lconstr_pattern_env env sigma t
 let pr_constr_pattern t =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   pr_constr_pattern_env env sigma t
 
 let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
@@ -253,11 +250,11 @@ let safe_gen f env sigma c =
 let safe_pr_lconstr_env = safe_gen pr_lconstr_env
 let safe_pr_constr_env = safe_gen pr_constr_env
 let safe_pr_lconstr t =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   safe_pr_lconstr_env env sigma t
 
 let safe_pr_constr t =
-  let (sigma, env) = get_current_context () in
+  let (sigma, env) = Pfedit.get_current_context () in
   safe_pr_constr_env env sigma t
 
 let pr_universe_ctx sigma c =
@@ -788,7 +785,7 @@ let pr_goal     x = !printer_pr.pr_goal     x
 (* End abstraction layer                                              *)
 (**********************************************************************)
 
-let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
+let pr_open_subgoals ~proof =
   (* spiwack: it shouldn't be the job of the printer to look up stuff
      in the [evar_map], I did stuff that way because it was more
      straightforward, but seriously, [Proof.proof] should return
@@ -826,15 +823,13 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
      pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused
   end
 
-let pr_nth_open_subgoal n =
-  let pf = Proof_global.give_me_the_proof () in
-  let gls,_,_,_,sigma = Proof.proof pf in
+let pr_nth_open_subgoal ~proof n =
+  let gls,_,_,_,sigma = Proof.proof proof in
   pr_subgoal n sigma gls
 
-let pr_goal_by_id id =
-  let p = Proof_global.give_me_the_proof () in
+let pr_goal_by_id ~proof id =
   try
-    Proof.in_proof p (fun sigma ->
+    Proof.in_proof proof (fun sigma ->
       let g = Evd.evar_key id sigma in
       pr_selected_subgoal (pr_id id) sigma g)
   with Not_found -> user_err Pp.(str "No such goal.")
@@ -916,7 +911,7 @@ let pr_assumptionset env s =
       with e when CErrors.noncritical e -> mt ()
     in
     let safe_pr_ltype_relctx (rctx, typ) =
-      let sigma, env = get_current_context () in
+      let sigma, env = Pfedit.get_current_context () in
       let env = Environ.push_rel_context rctx env in
       try str " " ++ pr_ltype_env env sigma typ
       with e when CErrors.noncritical e -> mt ()
diff --git a/printing/printer.mli b/printing/printer.mli
index fbba14ede..e014baa2c 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -27,10 +27,12 @@ val enable_goal_names_printing     : bool ref
 
 val pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
 val pr_lconstr             : constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
 val pr_constr_env          : env -> evar_map -> constr -> Pp.t
 val pr_constr              : constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
 val pr_constr_n_env        : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t
@@ -41,14 +43,18 @@ val pr_constr_n_env        : env -> evar_map -> Notation_term.tolerability -> co
 
 val safe_pr_lconstr_env         : env -> evar_map -> constr -> Pp.t
 val safe_pr_lconstr             : constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val safe_pr_constr_env          : env -> evar_map -> constr -> Pp.t
 val safe_pr_constr              : constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_econstr_env     : env -> evar_map -> EConstr.t -> Pp.t
 val pr_econstr         : EConstr.t -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 val pr_leconstr_env     : env -> evar_map -> EConstr.t -> Pp.t
 val pr_leconstr         : EConstr.t -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_econstr_n_env    : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t
 
@@ -57,41 +63,53 @@ val pr_letype_env           : env -> evar_map -> EConstr.types -> Pp.t
 
 val pr_open_constr_env     : env -> evar_map -> open_constr -> Pp.t
 val pr_open_constr         : open_constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_open_lconstr_env    : env -> evar_map -> open_constr -> Pp.t
 val pr_open_lconstr        : open_constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_constr_under_binders_env  : env -> evar_map -> constr_under_binders -> Pp.t
 val pr_constr_under_binders      : constr_under_binders -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t
 val pr_lconstr_under_binders     : constr_under_binders -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t
 val pr_ltype_env           : env -> evar_map -> types -> Pp.t
 val pr_ltype               : types -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_type_env            : env -> evar_map -> types -> Pp.t
 val pr_type                : types -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_closed_glob_n_env   : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t
 val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> Pp.t
 val pr_closed_glob         : closed_glob_constr -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_ljudge_env          : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t
 val pr_ljudge              : EConstr.unsafe_judgment -> Pp.t * Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_lglob_constr_env      : env -> 'a glob_constr_g -> Pp.t
 val pr_lglob_constr          : 'a glob_constr_g -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_glob_constr_env       : env -> 'a glob_constr_g -> Pp.t
 val pr_glob_constr           : 'a glob_constr_g -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t
 val pr_lconstr_pattern     : constr_pattern -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_constr_pattern_env  : env -> evar_map -> constr_pattern -> Pp.t
 val pr_constr_pattern      : constr_pattern -> Pp.t
+[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
 val pr_cases_pattern       : cases_pattern -> Pp.t
 
@@ -166,8 +184,8 @@ val pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> evar l
 val pr_subgoal             : int -> evar_map -> goal list -> Pp.t
 val pr_concl               : int -> evar_map -> goal -> Pp.t
 
-val pr_open_subgoals       : ?proof:Proof.proof -> unit -> Pp.t
-val pr_nth_open_subgoal    : int -> Pp.t
+val pr_open_subgoals       : proof:Proof.proof -> Pp.t
+val pr_nth_open_subgoal    : proof:Proof.proof -> int -> Pp.t
 val pr_evar                : evar_map -> (evar * evar_info) -> Pp.t
 val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> Pp.t
 val pr_evars               : evar_map -> evar_info Evar.Map.t -> Pp.t
@@ -200,13 +218,13 @@ module ContextObjectMap : CMap.ExtS
 val pr_assumptionset :
   env -> types ContextObjectMap.t -> Pp.t
 
-val pr_goal_by_id : Id.t -> Pp.t
+val pr_goal_by_id : proof:Proof.proof -> Id.t -> Pp.t
 
 type printer_pr = {
  pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t;
  pr_subgoal             : int -> evar_map -> goal list -> Pp.t;
  pr_goal                : goal sigma -> Pp.t;
-};;
+}
 
 val set_printer_pr : printer_pr -> unit
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 0abca0160..13a03e9b4 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -374,9 +374,12 @@ let rec print_typ_expr env mp locals mty =
   | MEwith(me,WithDef(idl,(c, _)))->
       let env' = None in (* TODO: build a proper environment if env <> None *)
       let s = String.concat "." (List.map Id.to_string idl) in
+      (* XXX: What should env and sigma be here? *)
+      let env = Global.env () in
+      let sigma = Evd.empty in
       hov 2 (print_typ_expr env' mp locals me ++ spc() ++ str "with" ++ spc()
              ++ def "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()
-             ++ Printer.pr_lconstr c)
+             ++ Printer.pr_lconstr_env env sigma c)
   | MEwith(me,WithMod(idl,mp'))->
       let s = String.concat "." (List.map Id.to_string idl) in
       hov 2 (print_typ_expr env mp locals me ++ spc() ++ str "with" ++ spc() ++