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

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

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

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

28 files changed, 236 insertions, 177 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index da8955f0d7..a09abfa193 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 bd5fb1d923..29e824f441 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 722dbc16b5..3899bc709c 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 8ab6dbcdf3..d04b7a33d1 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 dab094f913..f01b6669d7 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 61d207b953..8bf6e48fdb 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 692a874d36..694c800514 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 b372241d20..9e2774ff32 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 b8d41d539b..04d729b10c 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 89feea8dcf..bb01aca558 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 5baa0d5c1d..84e79d8abd 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 b148d962ed..91abe10190 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 3f885f8baa..d707512457 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 180fb2db40..918d1faebe 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 a669692fc9..2dd7c9a747 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 218342efe4..cb54cac3f1 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 430b608f4c..54ff44fbd3 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 05ab8ab326..a7d6d5bb20 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 9e4b896f8e..1c3bdb958f 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 c1d7e62785..83b4547698 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 26b5c57675..4e0b44a44d 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 e82f222b9c..274c7110c6 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 29e96ec59f..a707226cd0 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 023778fdbf..6c325cce43 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 7b591feada..46403aef3c 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 e865ef706d..4b2fab6d19 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 36dce37aea..cd614fee9d 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 d5c9e4988e..276b7c8ab2 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