Merge PR #6173: [printing] Deprecate all printing functions accessing the global proof.

57 files changed, 568 insertions, 413 deletions

diff --git a/API/API.mli b/API/API.mli
index 51671fc3d..86c6f1415 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -5150,12 +5150,20 @@ sig
   val pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.t
 
   val pr_constr : Constr.t -> Pp.t
+  [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
   val pr_lconstr : Constr.t -> Pp.t
+  [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
   val pr_econstr : EConstr.constr -> Pp.t
+  [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
+
   val pr_glob_constr : Glob_term.glob_constr -> Pp.t
+  [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
+
   val pr_constr_pattern : Pattern.constr_pattern -> Pp.t
+  [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
+
   val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t
   val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t
   val pr_econstr_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> EConstr.constr -> Pp.t
@@ -5163,11 +5171,17 @@ sig
   val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
   val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t
   val pr_closed_glob : Ltac_pretype.closed_glob_constr -> Pp.t
+  [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
   val pr_lglob_constr : Glob_term.glob_constr -> Pp.t
+  [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
   val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t
   val pr_leconstr : EConstr.constr -> Pp.t
+  [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
+
   val pr_global : Globnames.global_reference -> Pp.t
   val pr_lconstr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t
+  [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
+
   val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
 
   val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t
@@ -5176,7 +5190,11 @@ sig
   val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t
   val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t
   val pr_ltype : Term.types -> Pp.t
+  [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
+
   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_idpred : Names.Id.Pred.t -> Pp.t
   val pr_cpred : Names.Cpred.t -> Pp.t
   val pr_transparent_state : Names.transparent_state -> Pp.t
@@ -5689,7 +5707,9 @@ sig
   val create_hint_db : bool -> hint_db_name -> Names.transparent_state -> bool -> unit
   val empty_hint_info : 'a Vernacexpr.hint_info_gen
   val repr_hint : hint -> (raw_hint * Clenv.clausenv) hint_ast
+  val pr_hint_db_env : Environ.env -> Evd.evar_map -> Hint_db.t -> Pp.t
   val pr_hint_db : Hint_db.t -> Pp.t
+  [@@ocaml.deprecated "please used pr_hint_db_env"]
 end
 
 module Auto :
@@ -5766,7 +5786,7 @@ sig
   val add_rew_rules : string -> raw_rew_rule list -> unit
   val find_rewrites : string -> rew_rule list
   val find_matches : string -> Constr.t -> rew_rule list
-  val print_rewrite_hintdb : string -> Pp.t
+  val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t
 end
 
 (************************************************************************)
@@ -5799,11 +5819,12 @@ sig
     Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
   val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
   val get_current_context : unit -> Evd.evar_map * Environ.env
+  [@@ocaml.deprecated "please use [Pfedit.get_current_context]"]
 end
 
 module Himsg :
 sig
-  val explain_refiner_error : Logic.refiner_error -> Pp.t
+  val explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.t
   val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t
 end
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 5b09436c2..0f496d3b9 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -60,6 +60,7 @@ let pprecarg = function
 let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
 
 (* term printers *)
+let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma
 let rawdebug = ref false
 let ppevar evk = pp (str (Evd.string_of_existential evk))
 let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x))
@@ -69,9 +70,9 @@ let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.o
 let ppterm = ppconstr
 let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
-let ppglob_constr = (fun x -> pp(pr_lglob_constr x))
-let pppattern = (fun x -> pp(pr_constr_pattern x))
-let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))
+let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
+let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
+let pptype = (fun x -> try pp(envpp pr_ltype_env x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
 let ppbigint n = pp (str (Bigint.to_string n));;
@@ -121,7 +122,7 @@ let rec pr_closure {idents=idents;typed=typed;untyped=untyped} =
 and pr_closed_glob_constr_idmap x =
   pridmap (fun _ -> pr_closed_glob_constr) x
 and pr_closed_glob_constr {closure=closure;term=term} =
-  pr_closure closure ++ pr_lglob_constr term
+  pr_closure closure ++ (pr_lglob_constr_env Global.(env ())) term
 
 let ppclosure x = pp (pr_closure x)
 let ppclosedglobconstr x = pp (pr_closed_glob_constr x)
@@ -140,14 +141,14 @@ let safe_pr_global = function
 let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x
 
 let ppconst (sp,j) =
-    pp (str"#" ++ KerName.print sp ++ str"=" ++ pr_lconstr j.uj_val)
+    pp (str"#" ++ KerName.print sp ++ str"=" ++ envpp pr_lconstr_env j.uj_val)
 
 let ppvar ((id,a)) =
-    pp (str"#" ++ Id.print id ++ str":" ++ pr_lconstr a)
+    pp (str"#" ++ Id.print id ++ str":" ++ envpp pr_lconstr_env a)
 
 let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
 
-let ppj j = pp (genppj pr_ljudge j)
+let ppj j = pp (genppj (envpp pr_ljudge_env) j)
 
 let prsubst s = pp (Mod_subst.debug_pr_subst s)
 let prdelta s = pp (Mod_subst.debug_pr_delta s)
@@ -175,13 +176,13 @@ let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoalgoal gl = pp(Goal.pr_goal gl)
 let ppgoal g = pp(Printer.pr_goal g)
 let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g))
-let pphintdb db = pp(Hints.pr_hint_db db)
+let pphintdb db = pp(envpp Hints.pr_hint_db_env db)
 let ppproofview p =
   let gls,sigma = Proofview.proofview p in
   pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma)
 
 let ppopenconstr (x : Evd.open_constr) =
-  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ pr_constr c)
+  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_constr_env c)
 (* spiwack: deactivated until a replacement is found
 let pppftreestate p = pp(print_pftreestate p)
 *)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index d980b1995..51b06580e 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -60,6 +60,19 @@ val set_extern_reference :
 val get_extern_reference :
   unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
 
+(** WARNING: The following functions are evil due to
+    side-effects. Think of the following case as used in the printer:
+
+    without_specific_symbols [SynDefRule kn] (pr_glob_constr_env env) c
+
+    vs
+
+    without_specific_symbols [SynDefRule kn] pr_glob_constr_env env c
+
+    which one is wrong? We should turn this kind of state into an
+    explicit argument.
+*)
+
 (** This forces printing universe names of Type\{.\} *)
 val with_universes : ('a -> 'b) -> 'a -> 'b
 
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index da8955f0d..a09abfa19 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -200,7 +200,8 @@ module Btauto = struct
         let assign = List.combine env var in
         let map_msg (key, v) =
           let b = if v then str "true" else str "false" in
-          let term = Printer.pr_constr key in
+          let sigma, env = Pfedit.get_current_context () in
+          let term = Printer.pr_constr_env env sigma key in
           term ++ spc () ++ str ":=" ++ spc () ++ b
         in
         let assign = List.map map_msg assign in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bd5fb1d92..29e824f44 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -44,6 +44,10 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g
   *)
 
 
+let pr_leconstr_fp =
+  let sigma, env = Pfedit.get_current_context () in
+  Printer.pr_leconstr_env env sigma
+
 let debug_queue = Stack.create ()
 
 let rec print_debug_queue e = 
@@ -172,7 +176,7 @@ let is_incompatible_eq sigma t =
 	| _ -> false
     with e when CErrors.noncritical e -> false
   in
-  if res then   observe (str "is_incompatible_eq " ++ Printer.pr_leconstr t);
+  if res then   observe (str "is_incompatible_eq " ++ pr_leconstr_fp t);
   res
 
 let change_hyp_with_using msg hyp_id t tac : tactic =
@@ -220,7 +224,8 @@ let find_rectype env sigma c =
 let isAppConstruct ?(env=Global.env ()) sigma t =
   try
     let t',l = find_rectype env sigma t in
-    observe (str "isAppConstruct : " ++ Printer.pr_leconstr t ++ str " -> " ++ Printer.pr_leconstr (applist  (t',l)));
+    observe (str "isAppConstruct : " ++ Printer.pr_leconstr_env env sigma t ++ str " -> " ++
+             Printer.pr_leconstr_env env sigma (applist  (t',l)));
     true
   with Not_found -> false
 
@@ -233,7 +238,8 @@ exception NoChange
 let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
   let nochange ?t' msg  =
     begin
-      observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr t  ++ str "    " ++ match t' with None -> str "" | Some t -> Printer.pr_leconstr t );
+      observe (str ("Not treating ( "^msg^" )") ++ pr_leconstr_env env sigma t  ++ str "    " ++
+               match t' with None -> str "" | Some t -> Printer.pr_leconstr_env env sigma t );
       raise NoChange;
     end
   in
@@ -841,7 +847,7 @@ let build_proof
 	  | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!")
   and build_proof do_finalize dyn_infos g =
 (*     observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
-    observe_tac_stream (str "build_proof with " ++ Printer.pr_leconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
+    observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
   and build_proof_args do_finalize dyn_infos (* f_args'  args *) :tactic =
     fun g ->
       let (f_args',args) = dyn_infos.info in
@@ -1135,7 +1141,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	       princ_params
 	    );
     observe (str "fbody_with_full_params := " ++
-	       pr_leconstr fbody_with_full_params
+               pr_leconstr_env (Global.env ()) !evd fbody_with_full_params
 	    );
     let all_funs_with_full_params =
       Array.map (fun f -> applist(f, List.rev_map var_of_decl full_params)) all_funs
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 722dbc16b..3899bc709 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -115,7 +115,9 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let dummy_var = mkVar (Id.of_string "________") in
   let mk_replacement c i args =
     let res = mkApp(rel_to_fun.(i), Array.map pop (array_get_start args)) in
-    observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res);
+    observe (str "replacing " ++
+             pr_lconstr_env env Evd.empty c ++ str " by "  ++
+             pr_lconstr_env env Evd.empty res);
     res
   in
   let rec compute_new_princ_type remove env pre_princ : types*(constr list) =
@@ -565,7 +567,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
       List.map (* we can now compute the other principles *)
 	(fun scheme_type ->
 	   incr i;
-	   observe (Printer.pr_lconstr scheme_type);
+           observe (Printer.pr_lconstr_env env sigma scheme_type);
 	   let type_concl = (strip_prod_assum scheme_type) in
 	   let applied_f = List.hd (List.rev (snd (decompose_app type_concl))) in
 	   let f = fst (decompose_app applied_f) in
@@ -577,8 +579,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
 		let g = fst (decompose_app applied_g) in
 		if Constr.equal f g
 		then raise (Found_type j);
-		observe (Printer.pr_lconstr f ++ str " <> " ++
-			   Printer.pr_lconstr g)
+                observe (Printer.pr_lconstr_env env sigma f ++ str " <> " ++
+                         Printer.pr_lconstr_env env sigma g)
 
 	     )
 	     ta;
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8ab6dbcdf..d04b7a33d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -379,29 +379,30 @@ let add_pat_variables pat typ env : Environ.env =
     fst (
       Context.Rel.fold_outside
 	(fun decl (env,ctxt) ->
-         let open Context.Rel.Declaration in
-	 match decl with
+           let open Context.Rel.Declaration in
+           let sigma, _ = Pfedit.get_current_context () in
+           match decl with
 	   | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false
 	   | LocalAssum (Name id, t) ->
-	       let new_t =  substl ctxt t in
-	       observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
-			  str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
-			  str "new type := " ++ Printer.pr_lconstr new_t ++ fnl ()
-		       );
-               let open Context.Named.Declaration in
-	       (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
-	   | LocalDef (Name id, v, t) ->
-	       let new_t =  substl ctxt t in
-	       let new_v = substl ctxt v in
-	       observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
-			  str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
-			  str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
-			  str "old value := " ++ Printer.pr_lconstr v ++ fnl () ++
-			  str "new value := " ++ Printer.pr_lconstr new_v ++ fnl ()
-		       );
-               let open Context.Named.Declaration in
-	       (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt)
-      )
+             let new_t =  substl ctxt t in
+             observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
+                      str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
+                      str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl ()
+                     );
+             let open Context.Named.Declaration in
+             (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt)
+           | LocalDef (Name id, v, t) ->
+             let new_t =  substl ctxt t in
+             let new_v = substl ctxt v in
+             observe (str "for variable " ++ Ppconstr.pr_id id ++  fnl () ++
+                      str "old type := "  ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
+                      str "new type := "  ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ++
+                      str "old value := " ++ Printer.pr_lconstr_env env sigma v ++ fnl () ++
+                      str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl ()
+                     );
+             let open Context.Named.Declaration in
+             (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt)
+        )
 	(Environ.rel_context new_env)
 	~init:(env,[])
     )
@@ -479,7 +480,7 @@ let rec pattern_to_term_and_type env typ  = DAst.with_val (function
 
 
 let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
-  observe (str " Entering : " ++ Printer.pr_glob_constr rt);
+  observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt);
   let open CAst in
   match DAst.get rt with
     | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ ->
@@ -652,8 +653,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	  with Not_found ->
 	    user_err  (str "Cannot find the inductive associated to " ++
-			       Printer.pr_glob_constr b ++ str " in " ++
-			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
+                               Printer.pr_glob_constr_env env b ++ str " in " ++
+                               Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
 	in
 	let case_pats = build_constructors_of_type (fst ind) [] in
 	assert (Int.equal (Array.length case_pats) 2);
@@ -684,8 +685,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	    with Not_found ->
 	      user_err  (str "Cannot find the inductive associated to " ++
-				 Printer.pr_glob_constr b ++ str " in " ++
-				 Printer.pr_glob_constr rt ++ str ". try again with a cast")
+                                 Printer.pr_glob_constr_env env b ++ str " in " ++
+                                 Printer.pr_glob_constr_env env rt ++ str ". try again with a cast")
 	  in
 	  let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
 	  assert (Int.equal (Array.length case_pats) 1);
@@ -897,24 +898,24 @@ let same_raw_term rt1 rt2 =
     | GHole _, GHole _ -> true
     | _ -> false
 let decompose_raw_eq lhs rhs = 
-  let rec decompose_raw_eq lhs rhs acc = 
-    observe (str "decomposing eq for " ++ pr_glob_constr lhs ++ str " " ++ pr_glob_constr rhs);
-    let (rhd,lrhs) = glob_decompose_app rhs in 
-    let (lhd,llhs) = glob_decompose_app lhs in 
-    observe (str "lhd := " ++ pr_glob_constr lhd);
-    observe (str "rhd := " ++ pr_glob_constr rhd);
+  let _, env = Pfedit.get_current_context () in
+  let rec decompose_raw_eq lhs rhs acc =
+    observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs);
+    let (rhd,lrhs) = glob_decompose_app rhs in
+    let (lhd,llhs) = glob_decompose_app lhs in
+    observe (str "lhd := " ++ pr_glob_constr_env env lhd);
+    observe (str "rhd := " ++ pr_glob_constr_env env rhd);
     observe (str "llhs := " ++ int (List.length llhs));
     observe (str "lrhs := " ++ int (List.length lrhs));
-    let sllhs = List.length llhs in 
-    let slrhs = List.length lrhs in 
-    if same_raw_term lhd rhd && Int.equal sllhs slrhs 
+    let sllhs = List.length llhs in
+    let slrhs = List.length lrhs in
+    if same_raw_term lhd rhd && Int.equal sllhs slrhs
     then
       (* let _ = assert false in  *)
       List.fold_right2 decompose_raw_eq	llhs lrhs acc
     else (lhs,rhs)::acc
   in
   decompose_raw_eq lhs rhs []
-     
 
 exception Continue
 (*
@@ -923,7 +924,7 @@ exception Continue
    eliminates some meaningless equalities, applies some rewrites......
 *)
 let rec rebuild_cons env nb_args relname args crossed_types depth rt =
-  observe (str "rebuilding : " ++ pr_glob_constr rt);
+  observe (str "rebuilding : " ++ pr_glob_constr_env env rt);
   let open Context.Rel.Declaration in
   let open CAst in
   match DAst.get rt with
@@ -967,7 +968,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
                 let id = match DAst.get id with GVar id -> id | _ -> assert false in
 		begin
 		  try
-		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
+                    observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt);
 		    let t' =
 		      try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*)
                       with e when CErrors.noncritical e -> raise Continue
@@ -1012,7 +1013,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let eq' =
 		      DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
 		    in
-		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
+                    observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq');
 		    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
 		    observe (str " computing new type for jmeq : done") ;
 		    let new_args =
@@ -1099,7 +1100,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    rebuild_cons env nb_args relname args crossed_types depth new_rt
 		  else raise Continue
 	      with Continue -> 
-		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
+                observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
 		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
 		let new_env = Environ.push_rel (LocalAssum (n,t')) env in
 		let new_b,id_to_exclude =
@@ -1115,7 +1116,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	      end
 	    | _ ->
-		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
+                observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt);
 		let t',ctx = Pretyping.understand env (Evd.from_env env) t in
 		let new_env = Environ.push_rel (LocalAssum (n,t')) env in
 		let new_b,id_to_exclude =
@@ -1134,7 +1135,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_crossed_types = t :: crossed_types in
-	  observe (str "computing new type for lambda : " ++ pr_glob_constr rt);
+          observe (str "computing new type for lambda : " ++ pr_glob_constr_env env rt);
 	  let t',ctx = Pretyping.understand env (Evd.from_env env) t in
 	  match n with
 	    | Name id ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index dab094f91..f01b6669d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -46,7 +46,7 @@ let functional_induction with_clean c princl pat =
 		  try find_Function_infos c'
 		  with Not_found ->
 		    user_err  (str "Cannot find induction information on "++
-				       Printer.pr_leconstr (mkConst c') )
+                                       Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
 		in
 		match Tacticals.elimination_sort_of_goal g with
 		| InProp -> finfo.prop_lemma
@@ -74,7 +74,7 @@ let functional_induction with_clean c princl pat =
 		    (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
 		  with Not_found -> (* This one is neither defined ! *)
 		    user_err  (str "Cannot find induction principle for "
-				     ++Printer.pr_leconstr (mkConst c') )
+                                     ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
 	      in
 	      let princ = EConstr.of_constr princ in
 	      (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
@@ -841,12 +841,13 @@ let rec get_args b t : Constrexpr.local_binder_expr list *
 let make_graph (f_ref:global_reference) =
   let c,c_body =
     match f_ref with
-      | ConstRef c ->
-	  begin try c,Global.lookup_constant c
-	  with Not_found ->
-	    raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr (mkConst c)) )
-	  end
-      | _ -> raise (UserError (None, str "Not a function reference") )
+    | ConstRef c ->
+      begin try c,Global.lookup_constant c
+        with Not_found ->
+          let sigma, env = Pfedit.get_current_context () in
+          raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) )
+      end
+    | _ -> raise (UserError (None, str "Not a function reference") )
   in
   (match Global.body_of_constant_body c_body with
      | None -> error "Cannot build a graph over an axiom!"
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 61d207b95..8bf6e48fd 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -333,15 +333,17 @@ let discharge_Function (_,finfos) =
 	 }
 
 let pr_ocst c =
-  Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) c (mt ())
+  let sigma, env = Pfedit.get_current_context () in
+  Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ())
 
 let pr_info f_info =
+  let sigma, env = Pfedit.get_current_context () in
   str "function_constant := " ++
-  Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
+  Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++
   str "function_constant_type := " ++
   (try
-     Printer.pr_lconstr
-       (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant)))
+     Printer.pr_lconstr_env env sigma
+       (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant)))
    with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
   str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
   str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
@@ -349,7 +351,7 @@ let pr_info f_info =
   str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++
   str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++
   str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++
-  str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
+  str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl ()
 
 let pr_table tb =
   let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 692a874d3..694c80051 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -851,7 +851,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	   EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
 	 in
 	 let type_of_lemma = nf_zeta type_of_lemma in
-	 observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma);
+         observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma);
 	 type_of_lemma,type_info
 	)
 	funs_constr
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index b372241d2..9e2774ff3 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -90,20 +90,28 @@ let next_ident_fresh (id:Id.t) =
 (* comment this line to see debug msgs *)
 let msg x = () ;; let pr_lconstr c = str ""
 (* uncomment this to see debugging *)
-let prconstr c =  msg (str"  " ++ Printer.pr_lconstr c)
-let prconstrnl c =  msg (str"  " ++ Printer.pr_lconstr c ++ str"\n")
+let prconstr c   =
+  let sigma, env = Pfedit.get_current_context () in
+  msg (str"  " ++ Printer.pr_lconstr_env env sigma c)
+
+let prconstrnl c =
+  let sigma, env = Pfedit.get_current_context () in
+  msg (str"  " ++ Printer.pr_lconstr_env env sigma c ++ str"\n")
+
 let prlistconstr lc = List.iter prconstr lc
 let prstr s = msg(str s)
 let prNamedConstr s c =
+  let sigma, env = Pfedit.get_current_context () in
   begin
     msg(str "");
-    msg(str(s^" {§ ") ++ Printer.pr_lconstr c ++ str " §} ");
+    msg(str(s^" {§ ") ++ Printer.pr_lconstr_env env sigma c ++ str " §} ");
     msg(str "");
   end
 let prNamedRConstr s c =
+  let sigma, env = Pfedit.get_current_context () in
   begin
     msg(str "");
-    msg(str(s^" {§ ") ++ Printer.pr_glob_constr c ++ str " §} ");
+    msg(str(s^" {§ ") ++ Printer.pr_glob_constr_env env c ++ str " §} ");
     msg(str "");
   end
 let prNamedLConstr_aux lc = List.iter (prNamedConstr "\n") lc
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b8d41d539..04d729b10 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -54,6 +54,10 @@ let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@
 let arith_Nat = ["Arith";"PeanoNat";"Nat"]
 let arith_Lt = ["Arith";"Lt"]
 
+let pr_leconstr_rd =
+  let sigma, env = Pfedit.get_current_context () in
+  Printer.pr_leconstr_env env sigma
+
 let coq_init_constant s =
   EConstr.of_constr (
     Universes.constr_of_global @@
@@ -337,7 +341,8 @@ let check_not_nested sigma forbidden e =
   try 
     check_not_nested e 
   with UserError(_,p) -> 
-    user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr e ++ str " " ++ p)
+    let _, env = Pfedit.get_current_context () in
+    user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p)
 
 (* ['a info] contains the local information for traveling *)
 type 'a infos = 
@@ -455,7 +460,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
 	  check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info g
 	with e when CErrors.noncritical e ->
-	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
+          user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
       end
     | Lambda(n,t,b) -> 
       begin
@@ -463,7 +468,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
 	  check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info g
 	with e when CErrors.noncritical e ->
-	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
+          user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
       end
     | Case(ci,t,a,l) -> 
       begin
@@ -491,8 +496,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
 	      jinfo.apP (f,args) expr_info continuation_tac in 
 	    travel_args jinfo
 	      expr_info.is_main_branch new_continuation_tac new_infos g
-	  | Case _ ->  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
-	  | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr expr_info.info ++ Pp.str ".")
+          | Case _ ->  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
+          | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".")
       end
     | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g
     | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
@@ -515,7 +520,7 @@ and travel_args jinfo is_final continuation_tac infos =
 	{infos with info=arg;is_final=false} 
 and travel jinfo continuation_tac expr_info = 
   observe_tac 
-    (str jinfo.message ++ Printer.pr_leconstr expr_info.info) 
+    (str jinfo.message ++ pr_leconstr_rd expr_info.info)
     (travel_aux jinfo continuation_tac expr_info)
 
 (* Termination proof *) 
@@ -731,7 +736,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
   let destruct_tac,rev_to_thin_intro = 
     mkDestructEq [expr_info.rec_arg_id] a' g in 
   let to_thin_intro = List.rev rev_to_thin_intro in 
-  observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr a') 
+  observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a')
     (try
       (tclTHENS
 	 destruct_tac
@@ -740,7 +745,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
     with 
       | UserError(Some "Refiner.thensn_tac3",_) 
       | UserError(Some "Refiner.tclFAIL_s",_) ->
-	(observe_tac (str "is computable " ++ Printer.pr_leconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
+        (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
 	))
     g
     
@@ -991,11 +996,11 @@ let rec intros_values_eq expr_info acc =
 let equation_others _ expr_info continuation_tac infos = 
   if expr_info.is_final && expr_info.is_main_branch 
   then 
-    observe_tac (str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr expr_info.info)
+    observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info)
 		(tclTHEN 
       (continuation_tac infos) 
-      (observe_tac (str "intros_values_eq equation_others "  ++ Printer.pr_leconstr expr_info.info) (intros_values_eq expr_info [])))
-  else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_leconstr expr_info.info) (continuation_tac infos)
+      (observe_tac (str "intros_values_eq equation_others "  ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info [])))
+  else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos)
 
 let equation_app f_and_args expr_info continuation_tac infos = 
     if expr_info.is_final && expr_info.is_main_branch 
@@ -1419,7 +1424,7 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
-    let (evmap, env) = Lemmas.get_current_context() in
+    let evmap, env = Pfedit.get_current_context () in
     Lemmas.start_proof thm_name
       (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
       ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook;
@@ -1471,7 +1476,7 @@ let (com_eqn : int -> Id.t ->
 	| ConstRef c -> is_opaque_constant c
 	| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
     in
-    let (evmap, env) = Lemmas.get_current_context() in
+    let evmap, env = Pfedit.get_current_context () in
     let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 89feea8dc..bb01aca55 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -133,7 +133,9 @@ let pr_occurrences = pr_occurrences () () ()
 
 let pr_gen prc _prlc _prtac c = prc c
 
-let pr_globc _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr glob
+let pr_globc _prc _prlc _prtac (_,glob) =
+  let _, env = Pfedit.get_current_context () in
+  Printer.pr_glob_constr_env env glob
 
 let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
 
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 5baa0d5c1..84e79d8ab 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -51,8 +51,12 @@ let eval_uconstrs ist cs =
   List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
 
 let pr_auto_using_raw _ _ _  = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
-let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c)
-let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob
+let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) ->
+    let _, env = Pfedit.get_current_context () in
+    Printer.pr_glob_constr_env env c)
+let pr_auto_using _ _ _ = Pptactic.pr_auto_using
+    (let sigma, env = Pfedit.get_current_context () in
+     Printer.pr_closed_glob_env env sigma)
 
 ARGUMENT EXTEND auto_using
   TYPED AS uconstr_list
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index b148d962e..91abe1019 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -31,8 +31,12 @@ type constr_expr_with_bindings = constr_expr with_bindings
 type glob_constr_with_bindings = Tacexpr.glob_constr_and_expr with_bindings
 type glob_constr_with_bindings_sign = interp_sign * Tacexpr.glob_constr_and_expr with_bindings
 
-let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) = Printer.pr_glob_constr (fst (fst (snd ge)))
-let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge))
+let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) =
+  let _, env = Pfedit.get_current_context () in
+  Printer.pr_glob_constr_env env (fst (fst (snd ge)))
+let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) =
+  let _, env = Pfedit.get_current_context () in
+  Printer.pr_glob_constr_env env (fst (fst ge))
 let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge)
 let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c)
 let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l
@@ -272,5 +276,7 @@ TACTIC EXTEND setoid_transitivity
 END
 
 VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY
-  [ "Print" "Rewrite" "HintDb" preident(s) ] -> [ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) ]
+  [ "Print" "Rewrite" "HintDb" preident(s) ] ->
+  [ let sigma, env = Pfedit.get_current_context () in
+    Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) ]
 END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 3f885f8ba..d70751245 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1243,6 +1243,15 @@ let make_constr_printer f c =
 
 let lift f a = Genprint.PrinterBasic (fun () -> f a)
 
+
+let pr_glob_constr_pptac c =
+  let _, env = Pfedit.get_current_context () in
+  pr_glob_constr_env env c
+
+let pr_lglob_constr_pptac c =
+  let _, env = Pfedit.get_current_context () in
+  pr_lglob_constr_env env c
+
 let () =
   let pr_bool b = if b then str "true" else str "false" in
   let pr_unit _ = str "()" in
@@ -1257,7 +1266,7 @@ let () =
   Genprint.register_print0
     wit_intro_pattern
     (Miscprint.pr_intro_pattern pr_constr_expr)
-    (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
+    (Miscprint.pr_intro_pattern (fun (c, _) -> pr_glob_constr_pptac c))
     pr_intro_pattern_env;
   Genprint.register_print0
     wit_clause_dft_concl
@@ -1267,46 +1276,46 @@ let () =
   ;
   Genprint.register_print0
     wit_constr
-    Ppconstr.pr_lconstr_expr
-    (fun (c, _) -> Printer.pr_lglob_constr c)
+    Ppconstr.pr_constr_expr
+    (fun (c, _) -> pr_glob_constr_pptac c)
     (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0
     wit_uconstr
     Ppconstr.pr_constr_expr
-    (fun (c,_) -> Printer.pr_glob_constr c)
+    (fun (c, _) -> pr_glob_constr_pptac c)
     (make_constr_printer Printer.pr_closed_glob_n_env)
   ;
   Genprint.register_print0
     wit_open_constr
     Ppconstr.pr_constr_expr
-    (fun (c, _) -> Printer.pr_glob_constr c)
+    (fun (c, _) -> pr_glob_constr_pptac c)
     (make_constr_printer Printer.pr_econstr_n_env)
   ;
   Genprint.register_print0 wit_red_expr
     (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
-    (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
+    (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))
     pr_red_expr_env
   ;
   Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis);
   Genprint.register_print0 wit_bindings
     (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
-    (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
     pr_bindings_env
   ;
   Genprint.register_print0 wit_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
-    (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
     pr_with_bindings_env
   ;
   Genprint.register_print0 wit_open_constr_with_bindings
     (pr_with_bindings pr_constr_expr pr_lconstr_expr)
-    (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
     pr_with_bindings_env
   ;
   Genprint.register_print0 Tacarg.wit_destruction_arg
     (pr_destruction_arg pr_constr_expr pr_lconstr_expr)
-    (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))
     pr_destruction_arg_env
   ;
   Genprint.register_print0 Stdarg.wit_int int int (lift int);
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 180fb2db4..918d1faeb 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -91,9 +91,10 @@ let subst_global_reference subst =
  let subst_global ref =
   let ref',t' = subst_global subst ref in
    if not (is_global ref' t') then
-    Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
-          str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
-          pr_global ref') ;
+    (let sigma, env = Pfedit.get_current_context () in
+     Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
+          str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++
+          pr_global ref'));
    ref'
  in
   subst_or_var (subst_located subst_global)
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index a669692fc..2dd7c9a74 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -20,7 +20,9 @@ let prmatchpatt env sigma hyp =
   Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp
 let prmatchrl rl =
   Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env()))
-    (fun (_,p) -> Printer.pr_constr_pattern p) rl
+    (fun (_,p) ->
+       let sigma, env = Pfedit.get_current_context () in
+       Printer.pr_constr_pattern_env env sigma p) rl
 
 (* This module intends to be a beginning of debugger for tactic expressions.
    Currently, it is quite simple and we can hope to have, in the future, a more
@@ -369,7 +371,8 @@ let explain_ltac_call_trace last trace loc =
           strbrk " (with " ++
             prlist_with_sep pr_comma
             (fun (id,c) ->
-                Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
+              let sigma, env = Pfedit.get_current_context () in
+              Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c)
             (List.rev (Id.Map.bindings vars)) ++ str ")"
         else mt())
   in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 218342efe..cb54cac3f 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -984,7 +984,9 @@ struct
 
   let parse_expr sigma parse_constant parse_exp ops_spec env term =
     if debug
-    then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr term);
+    then (
+      let _, env = Pfedit.get_current_context () in
+      Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term));
 
 (*
     let constant_or_variable env term =
@@ -1103,9 +1105,10 @@ struct
     |  _ -> raise ParseError
 
 
-  let rconstant sigma term = 
+  let rconstant sigma term =
+    let _, env = Pfedit.get_current_context () in
     if debug
-    then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr term ++ fnl ());
+    then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ());
     let res = rconstant sigma term in
       if debug then 
 	(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1145,9 +1148,9 @@ struct
 
   let  parse_arith parse_op parse_expr env cstr gl =
     let sigma = gl.sigma in
-   if debug
-   then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ());
-   match EConstr.kind sigma cstr with
+    if debug
+    then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ());
+    match EConstr.kind sigma cstr with
     | Term.App(op,args) ->
        let (op,lhs,rhs) = parse_op gl (op,args) in
        let (e1,env) = parse_expr sigma env lhs in
@@ -1908,7 +1911,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
      let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
      let ff = dump_formula formula_typ
        (dump_cstr spec.typ spec.dump_coeff) ff in
-       Feedback.msg_notice (Printer.pr_leconstr ff);
+       Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff);
        Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
    end;
 
@@ -1932,9 +1935,9 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
       Feedback.msg_notice (Pp.str "\nAFormula\n") ;
       let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
       let ff' = dump_formula formula_typ
-        (dump_cstr spec.typ spec.dump_coeff) ff' in
-        Feedback.msg_notice (Printer.pr_leconstr ff');
-        Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
+          (dump_cstr spec.typ spec.dump_coeff) ff' in
+      Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff');
+      Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
     end;
 
   (* Even if it does not work, this does not mean it is not provable
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 430b608f4..54ff44fbd 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -183,8 +183,9 @@ let print_env_reification env =
   let rec loop c i = function
       [] ->  str "  ===============================\n\n"
     | t :: l ->
+      let sigma, env = Pfedit.get_current_context () in
       let s = Printf.sprintf "(%c%02d)" c i in
-      spc () ++ str s ++ str " := " ++ Printer.pr_lconstr t ++ fnl () ++
+      spc () ++ str s ++ str " := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++
       loop c (succ i) l
   in
   let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 05ab8ab32..a7d6d5bb2 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -82,10 +82,11 @@ VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
   | [ "Print" "Rings" ] => [Vernac_classifier.classify_as_query] -> [
     Feedback.msg_notice (strbrk "The following ring structures have been declared:");
     Spmap.iter (fun fn fi ->
+      let sigma, env = Pfedit.get_current_context () in
       Feedback.msg_notice (hov 2
         (Ppconstr.pr_id (Libnames.basename fn)++spc()++
-          str"with carrier "++ pr_constr fi.ring_carrier++spc()++
-          str"and equivalence relation "++ pr_constr fi.ring_req))
+          str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
+          str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
     ) !from_name ]
 END
 
@@ -117,10 +118,11 @@ VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
 | [ "Print" "Fields" ] => [Vernac_classifier.classify_as_query] -> [
     Feedback.msg_notice (strbrk "The following field structures have been declared:");
     Spmap.iter (fun fn fi ->
+      let sigma, env = Pfedit.get_current_context () in
       Feedback.msg_notice (hov 2
         (Ppconstr.pr_id (Libnames.basename fn)++spc()++
-          str"with carrier "++ pr_constr fi.field_carrier++spc()++
-          str"and equivalence relation "++ pr_constr fi.field_req))
+          str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
+          str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
     ) !field_from_name ]
 END
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9e4b896f8..1c3bdb958 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -344,8 +344,6 @@ let _ = add_map "ring"
 (****************************************************************************)
 (* Ring database *)
 
-let pr_constr c = pr_econstr c
-
 module Cmap = Map.Make(Constr)
 
 let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
@@ -368,7 +366,7 @@ let find_ring_structure env sigma l =
         with Not_found ->
           CErrors.user_err ~hdr:"ring"
             (str"cannot find a declared ring structure over"++
-             spc()++str"\""++pr_constr ty++str"\""))
+             spc() ++ str"\"" ++ pr_econstr_env env sigma ty ++ str"\""))
     | [] -> assert false
 
 let add_entry (sp,_kn) e =
@@ -529,19 +527,19 @@ let ring_equality env evd (r,add,mul,opp,req) =
 		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
 		  Flags.if_verbose
 		    Feedback.msg_info
-		    (str"Using setoid \""++pr_constr req++str"\""++spc()++
-			str"and morphisms \""++pr_constr add_m_lem ++
-			str"\","++spc()++ str"\""++pr_constr mul_m_lem++
-			str"\""++spc()++str"and \""++pr_constr opp_m_lem++
+                    (str"Using setoid \""++ pr_econstr_env env !evd req++str"\""++spc()++
+                        str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
+                        str"\","++spc()++ str"\""++pr_econstr_env env !evd mul_m_lem++
+                        str"\""++spc()++str"and \""++pr_econstr_env env !evd opp_m_lem++
 			str"\"");
 		  op_morph)
             | None ->
 		(Flags.if_verbose
 		    Feedback.msg_info
-		    (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++
-			str"and morphisms \""++pr_constr add_m_lem ++
+                    (str"Using setoid \""++pr_econstr_env env !evd req ++str"\"" ++ spc() ++
+                        str"and morphisms \""++pr_econstr_env env !evd add_m_lem ++
 			str"\""++spc()++str"and \""++
-			pr_constr mul_m_lem++str"\"");
+                        pr_econstr_env env !evd mul_m_lem++str"\"");
 		 op_smorph r add mul req add_m_lem mul_m_lem) in
           (setoid,op_morph)
 
@@ -861,7 +859,7 @@ let find_field_structure env sigma l =
         with Not_found ->
           CErrors.user_err ~hdr:"field"
             (str"cannot find a declared field structure over"++
-             spc()++str"\""++pr_constr ty++str"\""))
+             spc()++str"\""++pr_econstr_env env sigma ty++str"\""))
     | [] -> assert false
 
 let add_field_entry (sp,_kn) e =
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index c1d7e6278..83b454769 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -240,7 +240,7 @@ let interp_refine ist gl rc =
   in
   let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in
 (*   ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *)
-  ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr c));
+  ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c));
   (sigma, (sigma, c))
 
 
@@ -539,7 +539,7 @@ module Intset = Evar.Set
 
 let pf_abs_evars_pirrel gl (sigma, c0) =
   pp(lazy(str"==PF_ABS_EVARS_PIRREL=="));
-  pp(lazy(str"c0= " ++ Printer.pr_constr c0));
+  pp(lazy(str"c0= " ++ Printer.pr_constr_env (pf_env gl) sigma c0));
   let sigma0 = project gl in
   let c0 = nf_evar sigma0 (nf_evar sigma c0) in
   let nenv = env_size (pf_env gl) in
@@ -563,7 +563,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   | _ -> Constr.fold put evlist c in
   let evlist = put [] c0 in
   if evlist = [] then 0, c0 else
-  let pr_constr t = Printer.pr_econstr (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in
+  let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in
   pp(lazy(str"evlist=" ++ pr_list (fun () -> str";")
     (fun (k,_) -> str(Evd.string_of_existential k)) evlist));
   let evplist = 
@@ -959,7 +959,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
               loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1)
           | _ -> assert false
       in loop sigma t [] n in
-    pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr t));
+    pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
     Tacmach.refine_no_check t gl
 
 let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
@@ -973,7 +973,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
     compose_lam (let xs,y = List.chop (n-1) l in y @ xs) 
       (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n)))
   in
-  pp(lazy(str"after: " ++ Printer.pr_constr oc));
+  pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc));
   try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
   with e when CErrors.noncritical e -> raise dependent_apply_error
 
@@ -1202,7 +1202,7 @@ let genclrtac cl cs clr =
 let gentac ist gen gl =
 (*   ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *)
   let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux ist gl false gen in
-  ppdebug(lazy(str"c@gentac=" ++ pr_econstr c));
+  ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c));
   let gl = pf_merge_uc ucst gl in
   if conv
   then tclTHEN (Proofview.V82.of_tactic (convert_concl cl)) (cleartac clr) gl
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 26b5c5767..4e0b44a44 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -46,7 +46,7 @@ let analyze_eliminator elimty env sigma =
     if not (EConstr.eq_constr sigma t t') then loop ctx t' else
       errorstrm Pp.(str"The eliminator has the wrong shape."++spc()++
       str"A (applied) bound variable was expected as the conclusion of "++
-      str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr elimty) in
+      str"the eliminator's"++Pp.cut()++str"type:"++spc()++pr_econstr_env env' sigma elimty) in
   let ctx, pred_id, elim_is_dep, n_pred_args,concl = loop [] elimty in
   let n_elim_args = Context.Rel.nhyps ctx in
   let is_rec_elim = 
@@ -126,7 +126,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr
     ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern p));
     let (c,ucst), cl =
       fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in
-    ppdebug(lazy Pp.(str"     got: " ++ pr_constr c));
+    ppdebug(lazy Pp.(str"     got: " ++ pr_constr_env env sigma0 c));
     c, EConstr.of_constr cl, ucst in
   let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *)
     let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in 
@@ -239,8 +239,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) ?ist deps what ?elim eqid elim_intr
       | Some (c, _, _,gl) -> true, gl
       | None ->
         errorstrm Pp.(str"Unable to apply the eliminator to the term"++
-          spc()++pr_econstr c++spc()++str"or to unify it's type with"++
-          pr_econstr inf_arg_ty) in
+          spc()++pr_econstr_env env (project gl) c++spc()++str"or to unify it's type with"++
+          pr_econstr_env env (project gl) inf_arg_ty) in
   ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p));
   let gl, predty = pfe_type_of gl pred in
   (* Patterns for the inductive types indexes to be bound in pred are computed
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index e82f222b9..274c7110c 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -77,7 +77,7 @@ let interp_congrarg_at ist gl n rf ty m =
     if i + n > m then None else
     try
       let rt = mkRApp congrn (args1 @  mkRApp rf (mkRHoles i) :: args2) in
-      ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr rt));
+      ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) rt));
       Some (interp_refine ist gl rt)
     with _ -> loop (i + 1) in
   loop 0
@@ -86,7 +86,7 @@ let pattern_id = mk_internal_id "pattern value"
 
 let congrtac ((n, t), ty) ist gl =
   ppdebug(lazy (Pp.str"===congr==="));
-  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (Tacmach.pf_concl gl)));
+  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl)));
   let sigma, _ as it = interp_term ist gl t in
   let gl = pf_merge_uc_of sigma gl in
   let _, f, _, _ucst = pf_abs_evars gl it in
@@ -109,7 +109,7 @@ let congrtac ((n, t), ty) ist gl =
 
 let newssrcongrtac arg ist gl =
   ppdebug(lazy Pp.(str"===newcongr==="));
-  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr (pf_concl gl)));
+  ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl)));
   (* utils *)
   let fs gl t = Reductionops.nf_evar (project gl) t in
   let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl =
@@ -247,7 +247,7 @@ let unfoldintac occ rdx t (kt,_) gl =
       try find_T env c h ~k:(fun env c _ _ -> EConstr.Unsafe.to_constr (body env t (EConstr.of_constr c)))
       with NoMatch when easy -> c
       | NoMatch | NoProgress -> errorstrm Pp.(str"No occurrence of "
-        ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr c)),
+        ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ spc() ++ str "in " ++ Printer.pr_constr_env env sigma c)),
     (fun () -> try end_T () with 
       | NoMatch when easy -> fake_pmatcher_end () 
       | NoMatch -> anomaly "unfoldintac")
@@ -267,13 +267,13 @@ let unfoldintac occ rdx t (kt,_) gl =
             | Proj _ when same_proj sigma0 c t -> body env t c
             | Const f -> aux (body env c c)
             | App (f, a) -> aux (EConstr.mkApp (body env f f, a))
-            | _ -> errorstrm Pp.(str "The term "++pr_constr orig_c++
-                str" contains no " ++ pr_econstr t ++ str" even after unfolding")
+            | _ -> errorstrm Pp.(str "The term "++ pr_constr_env env sigma orig_c++
+                str" contains no " ++ pr_econstr_env env sigma t ++ str" even after unfolding")
           in EConstr.Unsafe.to_constr @@ aux (EConstr.of_constr c)
       else
         try EConstr.Unsafe.to_constr @@ body env t (fs (unify_HO env sigma (EConstr.of_constr c) t) t)
         with _ -> errorstrm Pp.(str "The term " ++
-          pr_constr c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))),
+          pr_constr_env env sigma c ++spc()++ str "does not unify with " ++ pr_constr_pat (EConstr.Unsafe.to_constr t))),
     fake_pmatcher_end in
   let concl = 
     let concl0 = EConstr.Unsafe.to_constr concl0 in
@@ -352,7 +352,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
   (* We check the proof is well typed *)
   let sigma, proof_ty =
     try Typing.type_of env sigma proof with _ -> raise PRtype_error in
-  ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr proof_ty));
+  ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty));
   try refine_with 
     ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl
   with _ -> 
@@ -374,8 +374,8 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
           if open_evs <> [] then Some name else None)
           (List.combine (Array.to_list args) names)
     | _ -> anomaly "rewrite rule not an application" in
-    errorstrm Pp.(Himsg.explain_refiner_error (Logic.UnresolvedBindings miss)++
-      (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr hd_ty))
+    errorstrm Pp.(Himsg.explain_refiner_error env sigma (Logic.UnresolvedBindings miss)++
+      (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty))
 ;;
 
 let is_construct_ref sigma c r =
@@ -391,12 +391,12 @@ let rwcltac cl rdx dir sr gl =
   let gl = pf_unsafe_merge_uc ucst gl in
   let rdxt = Retyping.get_type_of (pf_env gl) (fst sr) rdx in
 (*         ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *)
-        ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr (snd sr)));
+        ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env (pf_env gl) (project gl) (snd sr)));
   let cvtac, rwtac, gl =
     if EConstr.Vars.closed0 (project gl) r' then 
       let env, sigma, c, c_eq = pf_env gl, fst sr, snd sr, Coqlib.build_coq_eq () in
       let sigma, c_ty = Typing.type_of env sigma c in
-        ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr c_ty));
+        ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
       match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
       | AtomicType(e, a) when is_ind_ref sigma e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
@@ -411,7 +411,7 @@ let rwcltac cl rdx dir sr gl =
       let r3, _, r3t  = 
         try EConstr.destCast (project gl) r2 with _ ->
         errorstrm Pp.(str "no cast from " ++ pr_constr_pat (EConstr.Unsafe.to_constr (snd sr))
-                    ++ str " to " ++ pr_econstr r2) in
+                    ++ str " to " ++ pr_econstr_env (pf_env gl) (project gl) r2) in
       let cl' = EConstr.mkNamedProd rule_id (EConstr.it_mkProd_or_LetIn r3t dc) (EConstr.Vars.lift 1 cl) in
       let cl'' = EConstr.mkNamedProd pattern_id rdxt cl' in
       let itacs = [introid pattern_id; introid rule_id] in
@@ -605,7 +605,7 @@ let ssrinstancesofrule ist dir arg gl =
       sigma, pats @ [pat] in
     let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
     mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in
-  let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in
+  let print env p c _ = Feedback.msg_info Pp.(hov 1 (str"instance:" ++ spc() ++ pr_constr_env env r_sigma p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr_env env r_sigma c)); c in
   Feedback.msg_info Pp.(str"BEGIN INSTANCES");
   try
     while true do
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 29e96ec59..a707226cd 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -72,13 +72,14 @@ let examine_abstract id gl =
   let gl, tid = pfe_type_of gl id in
   let abstract, gl = pf_mkSsrConst "abstract" gl in
   let sigma = project gl in
+  let env = pf_env gl in
   if not (EConstr.isApp sigma tid) || not (EConstr.eq_constr sigma (fst(EConstr.destApp sigma tid)) abstract) then
-    errorstrm(strbrk"not an abstract constant: "++pr_econstr id);
+    errorstrm(strbrk"not an abstract constant: "++ pr_econstr_env env sigma id);
   let _, args_id = EConstr.destApp sigma tid in
   if Array.length args_id <> 3 then
-    errorstrm(strbrk"not a proper abstract constant: "++pr_econstr id);
+    errorstrm(strbrk"not a proper abstract constant: "++ pr_econstr_env env sigma id);
   if not (is_Evar_or_CastedMeta sigma args_id.(2)) then
-    errorstrm(strbrk"abstract constant "++pr_econstr id++str" already used");
+    errorstrm(strbrk"abstract constant "++ pr_econstr_env env sigma id++str" already used");
   tid, args_id
 
 let pf_find_abstract_proof check_lock gl abstract_n = 
@@ -94,7 +95,7 @@ let pf_find_abstract_proof check_lock gl abstract_n =
     | _ -> l) (project gl) [] in
   match l with
   | [e] -> e
-  | _ -> errorstrm(strbrk"abstract constant "++pr_constr abstract_n++
+  | _ -> errorstrm(strbrk"abstract constant "++ pr_constr_env (pf_env gl) (project gl) abstract_n ++
            strbrk" not found in the evar map exactly once. "++
            strbrk"Did you tamper with it?")
 
@@ -205,7 +206,7 @@ let havetac ist
      let assert_is_conv gl =
        try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl
        with _ -> errorstrm (str "Given proof term is not of type " ++
-         pr_econstr (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in
+         pr_econstr_env (pf_env gl) (project gl) (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in
      gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c
    | FwdHave, false, false ->
      let skols = List.flatten (List.map (function
@@ -271,7 +272,7 @@ let ssrabstract ist gens (*last*) gl =
     let gl, proof =
       let pf_unify_HO gl a b =
         try pf_unify_HO gl a b
-        with _ -> errorstrm(strbrk"The abstract variable "++pr_econstr id++
+        with _ -> errorstrm(strbrk"The abstract variable "++ pr_econstr_env env (project gl) id++
           strbrk" cannot abstract this goal.  Did you generalize it?") in
       let find_hole p t =
         match EConstr.kind (project gl) t with
@@ -290,7 +291,7 @@ let ssrabstract ist gens (*last*) gl =
         | App(hd, [|left; right|]) when Term.Constr.equal hd prod ->
             find_hole (mkApp (proj1,[|left;right;p|])) left
 *)
-        | _ -> errorstrm(strbrk"abstract constant "++pr_econstr abstract_n++
+        | _ -> errorstrm(strbrk"abstract constant "++ pr_econstr_env env (project gl) abstract_n++
                strbrk" has an unexpected shape. Did you tamper with it?")
       in
         find_hole
@@ -361,14 +362,14 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
       | Sort _, [] -> EConstr.Vars.subst_vars s ct
       | LetIn(Name id as n,b,ty,c), _::g -> EConstr.mkLetIn (n,b,ty,var2rel c g (id::s))
       | Prod(Name id as n,ty,c), _::g -> EConstr.mkProd (n,ty,var2rel c g (id::s))
-      | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr c) in
+      | _ -> CErrors.anomaly(str"SSR: wlog: var2rel: " ++ pr_econstr_env env sigma c) in
     let c = var2rel c gens [] in
     let rec pired c = function
       | [] -> c
       | t::ts as args -> match EConstr.kind sigma c with
          | Prod(_,_,c) -> pired (EConstr.Vars.subst1 t c) ts
          | LetIn(id,b,ty,c) -> EConstr.mkLetIn (id,b,ty,pired c args)
-         | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr c) in
+         | _ -> CErrors.anomaly(str"SSR: wlog: pired: " ++ pr_econstr_env env sigma c) in
     c, args, pired c args, pf_merge_uc uc gl in
   let tacipat pats = introstac ~ist pats in
   let tacigens = 
@@ -396,8 +397,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
       | Some id ->
         if pats = [] then Tacticals.tclIDTAC else
         let args = Array.of_list args in
-        ppdebug(lazy(str"specialized="++pr_econstr EConstr.(mkApp (mkVar id,args))));
-        ppdebug(lazy(str"specialized_ty="++pr_econstr ct));
+        ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args))));
+        ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct));
         Tacticals.tclTHENS (basecuttac "ssr_have" ct)
           [Proofview.V82.of_tactic (Tactics.apply EConstr.(mkApp (mkVar id,args))); Tacticals.tclIDTAC] in
       "ssr_have",
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 023778fdb..6c325cce4 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -272,7 +272,7 @@ let (introstac : ?ist:Tacinterp.interp_sign -> ssripats -> Tacmach.tactic),
 let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr gl =
   (* Utils of local interest only *)
   let iD s ?t gl = let t = match t with None -> pf_concl gl | Some x -> x in
-                   ppdebug(lazy Pp.(str s ++ pr_econstr t)); Tacticals.tclIDTAC gl in
+                   ppdebug(lazy Pp.(str s ++ pr_econstr_env (pf_env gl) (project gl) t)); Tacticals.tclIDTAC gl in
   let protectC, gl = pf_mkSsrConst "protect_term" gl in
   let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in
   let eq = EConstr.of_constr eq in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 7b591fead..46403aef3 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1131,7 +1131,7 @@ let pr_fwd_guarded prval prval' = function
 | (fk, h), (_, (_, Some c)) ->
   pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c)
 | (fk, h), (_, (c, None)) ->
-  pr_gen_fwd prval' pr_glob_constr prl_glob_constr fk (format_glob_constr h c)
+  pr_gen_fwd prval' pr_glob_constr_env prl_glob_constr fk (format_glob_constr h c)
 
 let pr_unguarded prc prlc = prlc
 
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index e865ef706..4b2fab6d1 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -24,7 +24,7 @@ let pp_concat hd ?(sep=str", ") = function [] -> hd | x :: xs ->
   hd ++ List.fold_left (fun acc x -> acc ++ sep ++ x) x xs
 
 let pp_term gl t =
-  let t = Reductionops.nf_evar (project gl) t in pr_econstr t
+  let t = Reductionops.nf_evar (project gl) t in pr_econstr_env (pf_env gl) (project gl) t
 
 (* FIXME *)
 (* terms are pre constr, the kind is parsing/printing flag to distinguish
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 36dce37ae..cd614fee9 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -343,7 +343,7 @@ let coerce_search_pattern_to_sort hpat =
   let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in
   let warn () =
     Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ 
-      pr_constr_pattern hpat') in
+      pr_constr_pattern_env env sigma hpat') in
   if EConstr.isSort sigma ht then begin warn (); true, hpat' end else
   let filter_head, coe_path =
     try 
@@ -359,7 +359,7 @@ let coerce_search_pattern_to_sort hpat =
       let n_imps = Option.get (Classops.hide_coercion coe_ref) in
       mkPApp (Pattern.PRef coe_ref) n_imps [|hp|]
     with _ ->
-    errorstrm (str "need explicit coercion " ++ pr_constr coe ++ spc ()
+    errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc ()
             ++ str "to interpret head search pattern as type") in
   filter_head, List.fold_left coerce hpat' coe_path
 
@@ -468,10 +468,12 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function
     prc c ++ str "|" ++ int (List.length args)
   | c -> prc c
 
-let pr_rawhintref c = match DAst.get c with
+let pr_rawhintref c =
+  let _, env = Pfedit.get_current_context () in
+  match DAst.get c with
   | GApp (f, args) when isRHoles args ->
-    pr_glob_constr f ++ str "|" ++ int (List.length args)
-  | _ -> pr_glob_constr c
+    pr_glob_constr_env env f ++ str "|" ++ int (List.length args)
+  | _ -> pr_glob_constr_env env c
 
 let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index d5c9e4988..276b7c8ab 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -100,7 +100,6 @@ let pr_guarded guard prc c =
   let s = Pp.string_of_ppcmds (prc c) ^ "$" in
   if guard s (skip_wschars s 0) then pr_paren prc c else prc c
 (* More sensible names for constr printers *)
-let pr_constr = pr_constr
 let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c
 let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c
 let prl_constr_expr = pr_lconstr_expr
@@ -427,7 +426,8 @@ let hole_var = mkVar (Id.of_string "_")
 let pr_constr_pat c0 =
   let rec wipe_evar c =
     if isEvar c then hole_var else map wipe_evar c in
-  pr_constr (wipe_evar c0)
+  let sigma, env = Pfedit.get_current_context () in
+  pr_constr_env env sigma (wipe_evar c0)
 
 (* Turn (new) evars into metas *)
 let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 =
@@ -1215,7 +1215,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst =
   let pop_evar sigma e p =
     let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in
     let e_body = match e_body with Evar_defined c -> c
-    | _ -> errorstrm (str "Matching the pattern " ++ pr_constr p ++
+    | _ -> errorstrm (str "Matching the pattern " ++ pr_constr_env env0 sigma0 p ++
           str " did not instantiate ?" ++ int (Evar.repr e) ++ spc () ++
           str "Does the variable bound by the \"in\" construct occur "++
           str "in the pattern?") in
@@ -1417,7 +1417,8 @@ let ssrinstancesof ist arg gl =
   let find, conclude =
     mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true
       sigma None (etpat,[tpat]) in
-  let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in
+  let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) p ++ spc()
+                                     ++ str "matches:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma)  c)); c in
   ppnl (str"BEGIN INSTANCES");
   try
     while true do
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() ++
diff --git a/stm/stm.ml b/stm/stm.ml
index 864fff9e0..a9cbcc9a6 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1931,9 +1931,10 @@ end = struct (* {{{ *)
           let open Notations in
           match Future.join f with
           | Some (pt, uc) ->
+            let sigma, env = Pfedit.get_current_context () in
             stm_pperr_endline (fun () -> hov 0 (
               str"g=" ++ int (Evar.repr gid) ++ spc () ++
-              str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
+              str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++
               str"uc=" ++ Termops.pr_evar_universe_context uc));
             (if abstract then Tactics.tclABSTRACT None else (fun x -> x))
               (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
diff --git a/tactics/auto.ml b/tactics/auto.ml
index d0424eb89..fa8435d1f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -388,7 +388,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
 	 Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
        else Tacticals.New.tclFAIL 0 (str"Unbound reference")
        end
-    | Extern tacast -> 
+    | Extern tacast ->
       conclPattern concl p tacast
   in
   let pr_hint () =
@@ -396,7 +396,8 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
     | None -> mt ()
     | Some n -> str " (in " ++ str n ++ str ")"
     in
-    pr_hint t ++ origin
+    let sigma, env = Pfedit.get_current_context () in
+    pr_hint env sigma t ++ origin
   in
   tclLOG dbg pr_hint (run_hint t tactic)
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index e68087f14..6a9cd7e20 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -74,12 +74,12 @@ let find_matches bas pat =
   let res = HintDN.search_pattern base pat in
   List.map snd res
 
-let print_rewrite_hintdb bas =
+let print_rewrite_hintdb env sigma bas =
   (str "Database " ++ str bas ++ fnl () ++
 	   prlist_with_sep fnl
 	   (fun h ->
 	     str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
-	       Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
+               Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++
 	       Option.cata (fun tac -> str " then use tactic " ++
 	       Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac)
 	   (find_rewrites bas))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index d2b5e070b..44acf3c01 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -40,7 +40,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni
 
 val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic
 
-val print_rewrite_hintdb : string -> Pp.t
+val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t
 
 open Clenv
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b98b10315..cee6d4bea 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -464,15 +464,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
       in
       let tac = run_hint t tac in
       let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
+      let _, env = Pfedit.get_current_context () in
       let pp =
         match p with
         | Some pat when get_typeclasses_filtered_unification () ->
-           str " with pattern " ++ Printer.pr_constr_pattern pat
+           str " with pattern " ++ Printer.pr_constr_pattern_env env sigma pat
         | _ -> mt ()
       in
         match repr_hint t with
-        | Extern _ -> (tac, b, true, name, lazy (pr_hint t ++ pp))
-        | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp))
+        | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp))
+        | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp))
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db secvars only_classes sigma concl =
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 239661498..f5c6ab879 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -178,7 +178,8 @@ and e_my_find_search sigma db_list local_db secvars hdc concl =
         | Extern tacast -> conclPattern concl p tacast
        in
        let tac = run_hint t tac in
-       (tac, lazy (pr_hint t)))
+       let sigma, env = Pfedit.get_current_context () in
+       (tac, lazy (pr_hint env sigma t)))
   in
   List.map tac_of_hint hintl
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 99be1846c..70e84013b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1392,14 +1392,14 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_hint_elt (c, _, _) = pr_econstr c
+let pr_hint_elt env sigma (c, _, _) = pr_econstr_env env sigma c
 
-let pr_hint h = match h.obj with
-  | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c)
-  | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt c)
-  | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c)
+let pr_hint env sigma h = match h.obj with
+  | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c)
+  | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt env sigma c)
+  | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c)
   | Res_pf_THEN_trivial_fail (c, _) ->
-      (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial")
+      (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial")
   | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
   | Extern tac ->
       let env =
@@ -1410,21 +1410,21 @@ let pr_hint h = match h.obj with
       in
       (str "(*external*) " ++ Pputils.pr_glb_generic env tac)
 
-let pr_id_hint (id, v) =
-  let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in
-  (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat
+let pr_id_hint env sigma (id, v) =
+  let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in
+  (pr_hint env sigma v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat
    ++ str", id " ++ int id ++ str ")" ++ spc ())
 
-let pr_hint_list hintlist =
-  (str "  " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ())
+let pr_hint_list env sigma hintlist =
+  (str "  " ++ hov 0 (prlist (pr_id_hint env sigma) hintlist) ++ fnl ())
 
-let pr_hints_db (name,db,hintlist) =
+let pr_hints_db env sigma (name,db,hintlist) =
   (str "In the database " ++ str name ++ str ":" ++
      if List.is_empty hintlist then (str " nothing" ++ fnl ())
-     else (fnl () ++ pr_hint_list hintlist))
+     else (fnl () ++ pr_hint_list env sigma hintlist))
 
 (* Print all hints associated to head c in any database *)
-let pr_hint_list_for_head c =
+let pr_hint_list_for_head env sigma c =
   let dbs = current_db () in
   let validate (name, db) =
     let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in
@@ -1436,13 +1436,13 @@ let pr_hint_list_for_head c =
   else
     hov 0
       (str"For " ++ pr_global c ++ str" -> " ++ fnl () ++
-	 hov 0 (prlist pr_hints_db valid_dbs))
+         hov 0 (prlist (pr_hints_db env sigma) valid_dbs))
 
 let pr_hint_ref ref = pr_hint_list_for_head ref
 
 (* Print all hints associated to head id in any database *)
 
-let pr_hint_term sigma cl =
+let pr_hint_term env sigma cl =
   try
     let dbs = current_db () in
     let valid_dbs =
@@ -1460,18 +1460,19 @@ let pr_hint_term sigma cl =
 	(str "No hint applicable for current goal")
       else
 	(str "Applicable Hints :" ++ fnl () ++
-	    hov 0 (prlist pr_hints_db valid_dbs))
+            hov 0 (prlist (pr_hints_db env sigma) valid_dbs))
   with Match_failure _ | Failure _ ->
     (str "No hint applicable for current goal")
 
 (* print all hints that apply to the concl of the current goal *)
 let pr_applicable_hint () =
+  let env = Global.env () in
   let pts = Proof_global.give_me_the_proof () in
   let glss,_,_,_,sigma = Proof.proof pts in
   match glss with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
   | g::_ ->
-    pr_hint_term sigma (Goal.V82.concl sigma g)
+    pr_hint_term env sigma (Goal.V82.concl sigma g)
 
 let pp_hint_mode = function
   | ModeInput -> str"+"
@@ -1479,9 +1480,9 @@ let pp_hint_mode = function
   | ModeOutput -> str"-"
 
 (* displays the whole hint database db *)
-let pr_hint_db db =
+let pr_hint_db_env env sigma db =
   let pr_mode = prvect_with_sep spc pp_hint_mode in
-  let pr_modes l = 
+  let pr_modes l =
     if List.is_empty l then mt ()
     else str" (modes " ++ prlist_with_sep pr_comma pr_mode l ++ str")"
   in
@@ -1491,7 +1492,7 @@ let pr_hint_db db =
       | None -> str "For any goal"
       | Some head -> str "For " ++ pr_global head ++ pr_modes modes
       in
-      let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in
+      let hints = pr_hint_list env sigma (List.map (fun x -> (0, x)) hintlist) in
       let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in
       accu ++ hint_descr
     in
@@ -1506,17 +1507,21 @@ let pr_hint_db db =
   hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++
   content
 
-let pr_hint_db_by_name dbname =
+let pr_hint_db db =
+  let sigma, env = Pfedit.get_current_context () in
+  pr_hint_db_env env sigma db
+
+let pr_hint_db_by_name env sigma dbname =
   try
-    let db = searchtable_map dbname in pr_hint_db db
+    let db = searchtable_map dbname in pr_hint_db_env env sigma db
   with Not_found ->
     error_no_such_hint_database dbname
 
 (* displays all the hints of all databases *)
-let pr_searchtable () =
+let pr_searchtable env sigma =
   let fold name db accu =
     accu ++ str "In the database " ++ str name ++ str ":" ++ fnl () ++
-    pr_hint_db db ++ fnl ()
+    pr_hint_db_env env sigma db ++ fnl ()
   in
   Hintdbmap.fold fold !searchtable (mt ())
 
@@ -1534,10 +1539,13 @@ let warn_non_imported_hint =
           strbrk "Hint used but not imported: " ++ hint ++ print_mp mp)
 
 let warn h x =
-  let hint = pr_hint h in
-  let (mp, _, _) = KerName.repr h.uid in
-  warn_non_imported_hint (hint,mp);
-  Proofview.tclUNIT x
+  let open Proofview in
+  tclBIND tclENV     (fun env   ->
+  tclBIND tclEVARMAP (fun sigma ->
+          let hint = pr_hint env sigma h in
+          let (mp, _, _) = KerName.repr h.uid in
+          warn_non_imported_hint (hint,mp);
+          Proofview.tclUNIT x))
 
 let run_hint tac k = match !warn_hint with
 | `LAX -> k tac.obj
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 22df29b80..cbf204981 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -260,14 +260,15 @@ val rewrite_db : hint_db_name
 
 (** Printing  hints *)
 
-val pr_searchtable : unit -> Pp.t
+val pr_searchtable : env -> evar_map -> Pp.t
 val pr_applicable_hint : unit -> Pp.t
-val pr_hint_ref : global_reference -> Pp.t
-val pr_hint_db_by_name : hint_db_name -> Pp.t
+val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t
+val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
+val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
 val pr_hint_db : Hint_db.t -> Pp.t
-val pr_hint : hint -> Pp.t
+[@@ocaml.deprecated "please used pr_hint_db_env"]
+val pr_hint : env -> evar_map -> hint -> Pp.t
 
 (** Hook for changing the initialization of auto *)
-
 val add_hints_init : (unit -> unit) -> unit
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 8648dfb90..46b10bf33 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -282,10 +282,11 @@ let generalizeRewriteIntros as_mode tac depids id =
 let error_too_many_names pats =
   let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in
   Proofview.tclENV >>= fun env ->
+  Proofview.tclEVARMAP >>= fun sigma ->
   tclZEROMSG ?loc (
     str "Unexpected " ++
     str (String.plural (List.length pats) "introduction pattern") ++
-    str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++
+    str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++
     str ".")
 
 let get_names (allow_conj,issimple) (loc, pat as x) = match pat with
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 15c25b346..e072bd95f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -945,10 +945,14 @@ let reduction_clause redexp cl =
 	(None, bind_red_expr_occurrences occs nbcl redexp)) cl
 
 let reduce redexp cl =
-  let trace () =
+  let trace env sigma =
     let open Printer in
-    let pr = (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern) in
-    Pp.(hov 2 (Pputils.pr_red_expr pr str redexp))
+    let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in
+    Pp.(hov 2 (Pputils.pr_red_expr_env env sigma pr str redexp))
+  in
+  let trace () =
+    let sigma, env = Pfedit.get_current_context () in
+    trace env sigma
   in
   Proofview.Trace.name_tactic trace begin
   Proofview.Goal.enter begin fun gl ->
@@ -3128,11 +3132,11 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
 
 let warn_unused_intro_pattern env sigma =
   CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics"
-         (fun names ->
-          strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern")
-          ++ str": " ++ prlist_with_sep spc 
-         (Miscprint.pr_intro_pattern 
-	 (fun c -> Printer.pr_econstr (snd (c env sigma)))) names)
+    (fun names ->
+       strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++
+       str": " ++ prlist_with_sep spc
+         (Miscprint.pr_intro_pattern
+            (fun c -> Printer.pr_econstr_env env sigma (snd (c env sigma)))) names)
 
 let check_unused_names env sigma names =
   if not (List.is_empty names) then
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f3d5d9b85..c61a1fd41 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -844,8 +844,10 @@ let start () =
     exit 1
   | _ ->
     flush_all();
-    if !output_context then
-      Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
+    if !output_context then begin
+      let sigma, env = Pfedit.get_current_context () in
+      Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
+    end;
     Profile.print_profile ();
     exit 0
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index cf63fbdc3..8fdaedbaf 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -100,7 +100,9 @@ let print_cmd_header ?loc com =
   Format.pp_print_flush !Topfmt.std_ft ()
 
 let pr_open_cur_subgoals () =
-  try Printer.pr_open_subgoals ()
+  try
+    let proof = Proof_global.give_me_the_proof () in
+    Printer.pr_open_subgoals ~proof
   with Proof_global.NoCurrentProof -> Pp.str ""
 
 (* Reenable when we get back to feedback printing *)
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 9e63df51d..51dd5cd4f 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -377,6 +377,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
   Proofview.Goal.enter begin fun gl ->
     let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in
     let sigma = Tacmach.New.project gl in
+    let env = Tacmach.New.pf_env gl in
     let u,v = destruct_ind sigma type_of_pq
     in let lb_type_of_p =
         try
@@ -389,7 +390,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
 	    (str "Leibniz->boolean:" ++
              str "You have to declare the" ++
 	     str "decidability over " ++
-	     Printer.pr_econstr type_of_pq ++
+             Printer.pr_econstr_env env sigma type_of_pq ++
 	     str " first.")
           in
           Tacticals.New.tclZEROMSG err_msg
@@ -442,6 +443,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
         Proofview.Goal.enter begin fun gl ->
         let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in
         let sigma = Tacmach.New.project gl in
+        let env = Tacmach.New.pf_env gl in
         if EConstr.eq_constr sigma t1 t2 then aux q1 q2
         else (
           let u,v = try  destruct_ind sigma tt1
@@ -461,7 +463,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
 	                                (str "boolean->Leibniz:" ++
                                          str "You have to declare the" ++
 			   	         str "decidability over " ++
-				         Printer.pr_econstr tt1 ++
+                                         Printer.pr_econstr_env env sigma tt1 ++
 				         str " first.")
 		 in
 		 user_err err_msg
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 2178a7caa..3a8e8fb43 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -76,7 +76,8 @@ let process_vernac_interp_error exn = match fst exn with
   | Tacred.ReductionTacticError e ->
       wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e)
   | Logic.RefinerError e ->
-      wrap_vernac_error exn (Himsg.explain_refiner_error e)
+    let sigma, env = Pfedit.get_current_context () in
+    wrap_vernac_error exn (Himsg.explain_refiner_error env sigma e)
   | Nametab.GlobalizationError q ->
       wrap_vernac_error exn
         (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index d15a811ba..839064aa0 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -92,9 +92,7 @@ let jv_nf_betaiotaevar sigma jl =
 
 (** Printers *)
 
-let pr_lconstr c = quote (pr_lconstr c)
 let pr_lconstr_env e s c = quote (pr_lconstr_env e s c)
-let pr_leconstr c = quote (pr_leconstr c)
 let pr_leconstr_env e s c = quote (pr_leconstr_env e s c)
 let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t)
 
@@ -1037,52 +1035,52 @@ let explain_typeclass_error env = function
 
 (* Refiner errors *)
 
-let explain_refiner_bad_type arg ty conclty =
+let explain_refiner_bad_type env sigma arg ty conclty =
   str "Refiner was given an argument" ++ brk(1,1) ++
-  pr_lconstr arg ++ spc () ++
-  str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++
-  str "instead of" ++ brk(1,1) ++ pr_lconstr conclty ++ str "."
+  pr_lconstr_env env sigma arg ++ spc () ++
+  str "of type" ++ brk(1,1) ++ pr_lconstr_env env sigma ty ++ spc () ++
+  str "instead of" ++ brk(1,1) ++ pr_lconstr_env env sigma conclty ++ str "."
 
 let explain_refiner_unresolved_bindings l =
   str "Unable to find an instance for the " ++
   str (String.plural (List.length l) "variable") ++ spc () ++
   prlist_with_sep pr_comma Name.print l ++ str"."
 
-let explain_refiner_cannot_apply t harg =
+let explain_refiner_cannot_apply env sigma t harg =
   str "In refiner, a term of type" ++ brk(1,1) ++
-  pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
-  pr_lconstr harg ++ str "."
+  pr_lconstr_env env sigma t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++
+  pr_lconstr_env env sigma harg ++ str "."
 
-let explain_refiner_not_well_typed c =
-  str "The term " ++ pr_lconstr c ++ str " is not well-typed."
+let explain_refiner_not_well_typed env sigma c =
+  str "The term " ++ pr_lconstr_env env sigma c ++ str " is not well-typed."
 
 let explain_intro_needs_product () =
   str "Introduction tactics needs products."
 
-let explain_does_not_occur_in c hyp =
-  str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++
+let explain_does_not_occur_in env sigma c hyp =
+  str "The term" ++ spc () ++ pr_lconstr_env env sigma c ++ spc () ++
   str "does not occur in" ++ spc () ++ Id.print hyp ++ str "."
 
-let explain_non_linear_proof c =
-  str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
+let explain_non_linear_proof env sigma c =
+  str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr_env env sigma c ++
   spc () ++ str "because a metavariable has several occurrences."
 
-let explain_meta_in_type c =
-  str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr c ++
+let explain_meta_in_type env sigma c =
+  str "In refiner, a meta appears in the type " ++ brk(1,1) ++ pr_leconstr_env env sigma c ++
   str " of another meta"
 
 let explain_no_such_hyp id =
   str "No such hypothesis: " ++ Id.print id
 
-let explain_refiner_error = function
-  | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
+let explain_refiner_error env sigma = function
+  | BadType (arg,ty,conclty) -> explain_refiner_bad_type env sigma arg ty conclty
   | UnresolvedBindings t -> explain_refiner_unresolved_bindings t
-  | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg
-  | NotWellTyped c -> explain_refiner_not_well_typed c
+  | CannotApply (t,harg) -> explain_refiner_cannot_apply env sigma t harg
+  | NotWellTyped c -> explain_refiner_not_well_typed env sigma c
   | IntroNeedsProduct -> explain_intro_needs_product ()
-  | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp
-  | NonLinearProof c -> explain_non_linear_proof c
-  | MetaInType c -> explain_meta_in_type c
+  | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in env sigma c hyp
+  | NonLinearProof c -> explain_non_linear_proof env sigma c
+  | MetaInType c -> explain_meta_in_type env sigma c
   | NoSuchHyp id -> explain_no_such_hyp id
 
 (* Inductive errors *)
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 5b91f9e68..8945ebadb 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -27,7 +27,7 @@ val explain_typeclass_error : env -> typeclass_error -> Pp.t
 
 val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t
 
-val explain_refiner_error : refiner_error -> Pp.t
+val explain_refiner_error : env -> Evd.evar_map -> refiner_error -> Pp.t
 
 val explain_pattern_matching_error :
   env -> Evd.evar_map -> pattern_matching_error -> Pp.t
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7b8a38d5f..a025bfff8 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -253,7 +253,9 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
         | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, body_i t2)
         | Lambda(na,ty,t) -> mkLambda(na,ty,body_i t)
         | App (t, args) -> mkApp (body_i t, args)
-        | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body ++ str ".") in
+        | _ ->
+          let sigma, env = Pfedit.get_current_context () in
+          anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in
       let body_i = body_i body in
       match locality with
       | Discharge ->
@@ -530,7 +532,5 @@ let save_proof ?proof = function
       Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
 
 (* Miscellaneous *)
+let get_current_context () = Pfedit.get_current_context ()
 
-let get_current_context () =
-  Pfedit.get_current_context ()
-           
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 6972edd52..1b1304db5 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -66,3 +66,4 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni
    and the current global env *)
 
 val get_current_context : unit -> Evd.evar_map * Environ.env
+[@@ocaml.deprecated "please use [Pfedit.get_current_context]"]
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c00b107cf..10c139e5a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -56,8 +56,9 @@ let scope_class_of_qualid qid =
 let show_proof () =
   (* spiwack: this would probably be cooler with a bit of polishing. *)
   let p = Proof_global.give_me_the_proof () in
+  let sigma, env = Pfedit.get_current_context () in
   let pprf = Proof.partial_proof p in
-  Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf)
+  Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
 
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
@@ -255,7 +256,8 @@ let print_namespace ns =
   let print_constant k body =
     (* FIXME: universes *)
     let t = body.Declarations.const_type in
-    print_kn k ++ str":" ++ spc() ++ Printer.pr_type t
+    let sigma, env = Pfedit.get_current_context () in
+    print_kn k ++ str":" ++ spc() ++ Printer.pr_type_env env sigma t
   in
   let matches mp = match match_modulepath ns mp with
   | Some [] -> true
@@ -484,8 +486,8 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
  	let red_option = match red_option with
           | None -> None
           | Some r ->
-	      let (evc,env)= get_current_context () in
- 		Some (snd (Hook.get f_interp_redexp env evc r)) in
+            let sigma, env= Pfedit.get_current_context () in
+            Some (snd (Hook.get f_interp_redexp env sigma r)) in
 	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
 
 let vernac_start_proof locality p kind l =
@@ -1537,7 +1539,7 @@ let vernac_print_option key =
 
 let get_current_context_of_args = function
   | Some n -> Pfedit.get_goal_context n
-  | None -> get_current_context ()
+  | None -> Pfedit.get_current_context ()
 
 let query_command_selector ?loc = function
   | None -> None
@@ -1626,17 +1628,20 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt =
     let natureofid = match decl with
                      | LocalAssum _ -> "Hypothesis"
                      | LocalDef (_,bdy,_) ->"Constant (let in)" in
-    v 0 (Id.print id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl()
+    let sigma, env = Pfedit.get_current_context () in
+    v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl()
 	 ++ str natureofid ++ str " of the goal context.")
   with (* fallback to globals *)
-    | NoHyp | Not_found -> print_about ref_or_by_not
+    | NoHyp | Not_found ->
+    let sigma, env = Pfedit.get_current_context () in
+    print_about env sigma ref_or_by_not
 
-	       
-let vernac_print ?loc = let open Feedback in function
+
+let vernac_print ?loc env sigma = let open Feedback in function
   | PrintTables -> msg_notice (print_tables ())
-  | PrintFullContext-> msg_notice (print_full_context_typ ())
-  | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid)
-  | PrintInspect n -> msg_notice (inspect n)
+  | PrintFullContext-> msg_notice (print_full_context_typ env sigma)
+  | PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid)
+  | PrintInspect n -> msg_notice (inspect env sigma n)
   | PrintGrammar ent -> msg_notice (Metasyntax.pr_grammar ent)
   | PrintLoadPath dir -> (* For compatibility ? *) msg_notice (print_loadpath dir)
   | PrintModules -> msg_notice (print_modules ())
@@ -1646,15 +1651,15 @@ let vernac_print ?loc = let open Feedback in function
   | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ())
   | PrintMLModules -> msg_notice (Mltop.print_ml_modules ())
   | PrintDebugGC -> msg_notice (Mltop.print_gc ())
-  | PrintName qid -> dump_global qid; msg_notice (print_name qid)
+  | PrintName qid -> dump_global qid; msg_notice (print_name env sigma qid)
   | PrintGraph -> msg_notice (Prettyp.print_graph())
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
   | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c))
-  | PrintCoercions -> msg_notice (Prettyp.print_coercions())
+  | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma)
   | PrintCoercionPaths (cls,clt) ->
       msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
-  | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ())
+  | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma)
   | PrintUniverses (b, dst) ->
      let univ = Global.universes () in
      let univ = if b then UGraph.sort_universes univ else univ in
@@ -1666,16 +1671,16 @@ let vernac_print ?loc = let open Feedback in function
      | None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
      | Some s -> dump_universes_gen univ s
      end
-  | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
+  | PrintHint r -> msg_notice (Hints.pr_hint_ref env sigma (smart_global r))
   | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
-  | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s)
-  | PrintHintDb -> msg_notice (Hints.pr_searchtable ())
+  | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name env sigma s)
+  | PrintHintDb -> msg_notice (Hints.pr_searchtable env sigma)
   | PrintScopes ->
-      msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
+      msg_notice (Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env)))
   | PrintScope s ->
-      msg_notice (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s)
+      msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
   | PrintVisibility s ->
-      msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
+      msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
   | PrintAbout (ref_or_by_not,glnumopt) ->
      msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt)
   | PrintImplicit qid ->
@@ -1778,9 +1783,10 @@ let vernac_locate = let open Feedback in function
   | LocateTerm (AN qid) -> msg_notice (print_located_term qid)
   | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *)
   | LocateTerm (ByNotation (_, (ntn, sc))) ->
-      msg_notice
-        (Notation.locate_notation
-          (Constrextern.without_symbols pr_lglob_constr) ntn sc)
+    let _, env = Pfedit.get_current_context () in
+    msg_notice
+      (Notation.locate_notation
+         (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc)
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> msg_notice (print_located_module qid)
   | LocateOther (s, qid) -> msg_notice (print_located_other s qid)
@@ -1847,10 +1853,11 @@ let vernac_bullet (bullet : Proof_bullet.t) =
 let vernac_show = let open Feedback in function
   | ShowScript -> assert false  (* Only the stm knows the script *)
   | ShowGoal goalref ->
+    let proof = Proof_global.give_me_the_proof () in
     let info = match goalref with
-      | OpenSubgoals -> pr_open_subgoals ()
-      | NthGoal n -> pr_nth_open_subgoal n
-      | GoalId id -> pr_goal_by_id id
+      | OpenSubgoals -> pr_open_subgoals ~proof
+      | NthGoal n -> pr_nth_open_subgoal ~proof n
+      | GoalId id -> pr_goal_by_id ~proof id
     in
     msg_notice info
   | ShowProof -> show_proof ()
@@ -2041,7 +2048,9 @@ let interp ?proof ?loc locality poly st c =
   | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ?loc r g c
   | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r
   | VernacGlobalCheck c -> vernac_global_check c
-  | VernacPrint p -> vernac_print ?loc p
+  | VernacPrint p ->
+    let sigma, env = Pfedit.get_current_context () in
+    vernac_print ?loc env sigma p
   | VernacSearch (s,g,r) -> vernac_search ?loc s g r
   | VernacLocate l -> vernac_locate l
   | VernacRegister (id, r) -> vernac_register id r