[print] Restrict use of "debug" Termops printer.

The functions in `Termops.print_*` are meant to be debug printers,
however, they are sometimes used in non-debug code due to a API
confusion.

We thus wrap such functions into an `Internal` module, improve
documentation, and switch users to the right API.

20 files changed, 111 insertions, 54 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 4f3d793ed4..fdeb0abed4 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,12 @@
+## Changes between Coq 8.9 and Coq 8.10
+
+### ML API
+
+Termops:
+
+- Internal printing functions have been placed under the
+  `Termops.Internal` namespace.
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ab679a71ce..ced6ea2614 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -64,8 +64,14 @@ let ppwf_paths x = pp (Rtree.pp_tree prrecarg x)
 let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma
 let rawdebug = ref false
 let ppevar evk = pp (Evar.print evk)
-let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x))
-let ppeconstr x = pp (Termops.print_constr x)
+let pr_constr t =
+  let sigma, env = Pfedit.get_current_context () in
+  Printer.pr_constr_env env sigma t
+let pr_econstr t =
+  let sigma, env = Pfedit.get_current_context () in
+  Printer.pr_econstr_env env sigma t
+let ppconstr x = pp (pr_constr x)
+let ppeconstr x = pp (pr_econstr x)
 let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
 let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
@@ -95,9 +101,9 @@ let ppidmapgen l = pp (pridmapgen l)
 
 let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) ->
   hov 0
-  (Termops.print_constr (EConstr.of_constr c) ++
+  (pr_constr c ++
    (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++
-    Termops.print_constr (EConstr.of_constr c) ++ str">") ++
+    pr_constr c ++ str">") ++
    (if id = id0 then mt ()
     else spc () ++ str "<canonical: " ++ Id.print id ++ str ">"))))
 
@@ -106,7 +112,7 @@ let ppididmap = ppidmap (fun _ -> Id.print)
 
 let prconstrunderbindersidmap = pridmap (fun _ (l,c) ->
   hov 1 (str"[" ++  prlist_with_sep spc Id.print l ++ str"]")
-  ++ str "," ++ spc () ++ Termops.print_constr c)
+  ++ str "," ++ spc () ++ pr_econstr c)
 
 let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l)
 
@@ -155,9 +161,9 @@ let ppdelta s = pp (Mod_subst.debug_pr_delta s)
 let pp_idpred s = pp (pr_idpred s)
 let pp_cpred s = pp (pr_cpred s)
 let pp_transparent_state s = pp (pr_transparent_state s)
-let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> Termops.print_constr) n)
-let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n)
-let pp_state_t n = pp (Reductionops.pr_state n)
+let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n)
+let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr Global.(env()) Evd.empty n)
+let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
 
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
diff --git a/engine/termops.ml b/engine/termops.ml
index 710743e92d..efe1525c9a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -22,6 +22,8 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 module CompactedDecl = Context.Compacted.Declaration
 
+module Internal = struct
+
 (* Sorts and sort family *)
 
 let print_sort = function
@@ -98,12 +100,16 @@ let rec pr_constr c = match kind c with
            cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
          str"}")
 
-let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c))
+let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c)
+let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c)
+let term_printer = ref debug_print_constr_env
+
 let print_constr_env env sigma t = !term_printer env sigma t
 let print_constr t =
   let env = Global.env () in
   let evd = Evd.from_env env in
   !term_printer env evd t
+
 let set_print_constr f = term_printer := f
 
 module EvMap = Evar.Map
@@ -1537,3 +1543,6 @@ let env_rel_context_chop k env =
   let ctx1,ctx2 = List.chop k rels in
   push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
   ctx1
+end
+
+include Internal
diff --git a/engine/termops.mli b/engine/termops.mli
index 9ce2db9234..aa0f837938 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -311,18 +311,40 @@ val pr_metaset : Metaset.t -> Pp.t
 val pr_evar_universe_context : UState.t -> Pp.t
 val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t
 
-(** Internal hook to register user-level printer *)
+module Internal : sig
 
-val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
+(** NOTE: to print terms you always want to use functions in
+   Printer, not these ones which are for very special cases. *)
 
-(** User-level printers *)
+(** debug printers: print raw form for terms, both with
+   evar-substitution and without.  *)
+val debug_print_constr : constr -> Pp.t
+val debug_print_constr_env : env -> evar_map -> constr -> Pp.t
 
-val print_constr     : constr -> Pp.t
+(** Pretty-printer hook: [print_constr_env env sigma c] will pretty
+   print c if the pretty printing layer has been linked into the Coq
+   binary. *)
 val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
 
-(** debug printer: do not use to display terms to the casual user... *)
+(** [set_print_constr f] sets f to be the pretty printer *)
+val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit
 
+(** Printers for contexts *)
 val print_named_context : env -> Pp.t
 val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t
 val print_rel_context : env -> Pp.t
 val print_env : env -> Pp.t
+
+val print_constr : constr -> Pp.t
+[@@deprecated "use print_constr_env"]
+
+end
+
+val print_constr : constr -> Pp.t
+[@@deprecated "use Internal.print_constr_env"]
+
+val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t
+[@@deprecated "use Internal.print_constr_env"]
+
+val print_rel_context : env -> Pp.t
+[@@deprecated "use Internal.print_rel_context"]
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index ce620d5312..f26ec0f401 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -26,6 +26,10 @@ let init_size=5
 
 let cc_verbose=ref false
 
+let print_constr t =
+  let sigma, env = Pfedit.get_current_context () in
+  Printer.pr_econstr_env env sigma t
+
 let debug x =
   if !cc_verbose then Feedback.msg_debug (x ())
 
@@ -483,10 +487,10 @@ let rec inst_pattern subst = function
 	   args t
 
 let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++
-  Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
+  print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]"
 
 let pr_term t = str "[" ++
-  Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
+  print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]"
 
 let rec add_term state t=
   let uf=state.uf in
@@ -601,7 +605,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
+                  (str "  [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " == " ++ pr_term t ++ str "]"));
 		add_equality state prf s t
 	      end
@@ -609,7 +613,7 @@ let add_inst state (inst,int_subst) =
 	      begin
 		debug (fun () ->
 		   (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
-	          (str "  [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++
+                  (str "  [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++
 			   pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
 		add_disequality state (Hyp prf) s t
 	      end
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 48d677a864..6bab8d0353 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -12,7 +12,6 @@ open Util
 open Names
 open Pp
 open Tacexpr
-open Termops
 
 let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
 
@@ -51,8 +50,8 @@ let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl())
 let db_pr_goal gl =
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
-  let penv = print_named_context env in
-  let pc = print_constr_env env (Tacmach.New.project gl) concl in
+  let penv = Termops.Internal.print_named_context env in
+  let pc = Printer.pr_econstr_env env (Tacmach.New.project gl) concl in
     str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
@@ -243,7 +242,7 @@ let db_constr debug env sigma c =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str "Evaluated term: " ++ print_constr_env env sigma c)
+    msg_tac_debug (str "Evaluated term: " ++ Printer.pr_econstr_env env sigma c)
   else return ()
 
 (* Prints the pattern rule *)
@@ -268,7 +267,7 @@ let db_matched_hyp debug env sigma (id,_,c) ido =
   is_debug debug >>= fun db ->
   if db then
     msg_tac_debug (str "Hypothesis " ++ Id.print id ++ hyp_bound ido ++
-                str " has been matched: " ++ print_constr_env env sigma c)
+                str " has been matched: " ++ Printer.pr_econstr_env env sigma c)
   else return ()
 
 (* Prints the matched conclusion *)
@@ -276,7 +275,7 @@ let db_matched_concl debug env sigma c =
   let open Proofview.NonLogical in
   is_debug debug >>= fun db ->
   if db then
-    msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env sigma c)
+    msg_tac_debug (str "Conclusion has been matched: " ++ Printer.pr_econstr_env env sigma c)
   else return ()
 
 (* Prints a success message when the goal has been matched *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6c52dacaa9..7d480b8d48 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -588,7 +588,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
   (* Evar must be undefined since we have flushed evars *)
   let () = if !debug_unification then
 	     let open Pp in
-	     Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in
+             Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
   match (flex_kind_of_term (fst ts) env evd term1 sk1, 
 	 flex_kind_of_term (fst ts) env evd term2 sk2) with
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
@@ -1225,8 +1225,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
   let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
   let () = if !debug_unification then
 	     let open Pp in
-	     Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1
-                                       ++ cut () ++ print_constr t2 ++ cut ())) in
+             Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++
+                                Termops.Internal.print_constr_env env evd t1 ++ cut () ++
+                                Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
   let app_empty = Array.is_empty l1 && Array.is_empty l2 in
   match EConstr.kind evd term1, EConstr.kind evd term2 with
   | Evar (evk1,args1), (Rel _|Var _) when app_empty
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index b452755b10..571be7466c 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -201,4 +201,4 @@ let lift_tycon n = Option.map (lift n)
 
 let pr_tycon env sigma = function
     None -> str "None"
-  | Some t -> Termops.print_constr_env env sigma t
+  | Some t -> Termops.Internal.print_constr_env env sigma t
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 25510826cc..63a66b471b 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -140,7 +140,7 @@ let protected_get_type_of env sigma c =
   try Retyping.get_type_of ~lax:true env sigma c
   with Retyping.RetypeError _ ->
     user_err
-      (str "Cannot reinterpret " ++ quote (print_constr c) ++
+      (str "Cannot reinterpret " ++ quote (Termops.Internal.print_constr_env env sigma c) ++
        str " in the current environment.")
 
 let invert_ltac_bound_name env id0 id =
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index b040e63cd2..0fa573b9a6 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -358,7 +358,7 @@ let make_case_or_project env sigma indf ci pred c branches =
           not (has_dependent_elim mib) then
        user_err ~hdr:"make_case_or_project"
                     Pp.(str"Dependent case analysis not allowed" ++
-                     str" on inductive type " ++ print_constr_env env sigma (mkInd ind))
+                     str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind))
      in
      let branch = branches.(0) in
      let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a4c2cb2352..b9345190fb 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -976,9 +976,9 @@ and pretype_instance k0 resolve_tc env evdref loc hyps evk update =
              pr_existential_key !evdref evk ++
              strbrk " in current context: binding for " ++ Id.print id ++
              strbrk " is not convertible to its expected definition (cannot unify " ++
-             quote (print_constr_env !!env !evdref b) ++
+             quote (Termops.Internal.print_constr_env !!env !evdref b) ++
              strbrk " and " ++
-             quote (print_constr_env !!env !evdref c) ++
+             quote (Termops.Internal.print_constr_env !!env !evdref c) ++
              str ").")
       | Some b, None ->
            user_err ?loc  (str "Cannot interpret " ++
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 77ad96d2cf..c25416405e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -229,7 +229,7 @@ let warn_projection_no_head_constant =
           let env = Termops.push_rels_assum sign env in
           let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
           let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
-          let term_pp = Termops.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
+          let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in
           strbrk "Projection value has no head constant: "
           ++ term_pp ++ strbrk " in canonical instance "
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
@@ -295,8 +295,12 @@ let add_canonical_structure warn o =
       in match ocs with
         | None -> object_table := GlobRef.Map.add proj ((pat,s)::l) !object_table;
         | Some (c, cs) ->
-              let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF))
-              and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in
+              (* XXX: Undesired global access to env *)
+              let env = Global.env () in
+              let sigma = Evd.from_env env in
+              let old_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF))
+              and new_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF))
+              in
               let prj = (Nametab.pr_global_env Id.Set.empty proj)
               and hd_val = (pr_cs_pattern cs_pat) in
               if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s))
@@ -362,7 +366,7 @@ let check_and_decompose_canonical_structure ref =
     try lookup_structure indsp
     with Not_found ->
       error_not_structure ref
-        (str "Could not find the record or structure " ++ Termops.print_constr (EConstr.mkInd indsp)) in
+        (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env evd (EConstr.mkInd indsp)) in
   let ntrue_projs = List.count snd s.s_PROJKIND in
   if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
     error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a0d20b7ce4..e8c3b3e2b3 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -254,9 +254,9 @@ module Cst_stack = struct
 	(applist (cst, List.rev params))
 	t) cst_l c
 
-  let pr l =
+  let pr env sigma l =
     let open Pp in
-    let p_c c = Termops.print_constr c in
+    let p_c c = Termops.Internal.print_constr_env env sigma c in
     prlist_with_sep pr_semicolon
       (fun (c,params,args) ->
 	hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++
@@ -615,9 +615,9 @@ type contextual_state_reduction_function =
 type state_reduction_function = contextual_state_reduction_function
 type local_state_reduction_function = evar_map -> state -> state
 
-let pr_state (tm,sk) =
+let pr_state env sigma (tm,sk) =
   let open Pp in
-  let pr c = Termops.print_constr c in
+  let pr c = Termops.Internal.print_constr_env env sigma c in
   h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk)
 
 (*************************************)
@@ -855,10 +855,10 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   let rec whrec cst_l (x, stack) =
     let () = if !debug_RAKAM then
 	let open Pp in
-	let pr c = Termops.print_constr c in
+        let pr c = Termops.Internal.print_constr_env env sigma c in
 	Feedback.msg_notice
              (h 0 (str "<<" ++ pr x ++
-		   str "|" ++ cut () ++ Cst_stack.pr cst_l ++
+                   str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++
 		   str "|" ++ cut () ++ Stack.pr pr stack ++
 		   str ">>"))
     in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index dd3cd26f0f..c0ff6723f6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -60,7 +60,7 @@ module Cst_stack : sig
   val best_cst : t -> (constr * constr list) option
   val best_replace : Evd.evar_map -> constr -> t -> constr -> constr
   val reference : Evd.evar_map -> t -> Constant.t option
-  val pr : t -> Pp.t
+  val pr : env -> Evd.evar_map -> t -> Pp.t
 end
 
 module Stack : sig
@@ -140,7 +140,7 @@ type contextual_state_reduction_function =
 type state_reduction_function = contextual_state_reduction_function
 type local_state_reduction_function = evar_map -> state -> state
 
-val pr_state : state -> Pp.t
+val pr_state : env -> evar_map -> state -> Pp.t
 
 (** {6 Reduction Function Operators } *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index fc1f6fc81e..e223674579 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -684,8 +684,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     and cN = Evarutil.whd_head_evar sigma curn in
     let () = 
       if !debug_unification then
-	Feedback.msg_debug (print_constr_env curenv sigma cM ++ str" ~= " ++ print_constr_env curenv sigma cN)
-    in 
+        Feedback.msg_debug (
+          Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++
+          Termops.Internal.print_constr_env curenv sigma cN)
+    in
       match (EConstr.kind sigma cM, EConstr.kind sigma cN) with
 	| Meta k1, Meta k2 ->
             if Int.equal k1 k2 then substn else
diff --git a/printing/printer.ml b/printing/printer.ml
index 5ca330d377..b4038e0ff9 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -192,7 +192,7 @@ let pr_constr_pattern t =
 
 let pr_sort sigma s = pr_glob_sort (extern_sort sigma s)
 
-let _ = Termops.set_print_constr 
+let _ = Termops.Internal.set_print_constr
   (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t))
 
 let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 79b7e1599b..95e908c4dd 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -575,8 +575,8 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 
 let pr_clenv clenv =
   h 0
-    (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
-     str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
+    (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++
+     str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++
      pr_evar_map (Some 2) clenv.evd)
 
 (****************************************************************)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 092bb5c276..182b38d350 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -127,8 +127,8 @@ open Pp
 
 let db_pr_goal sigma g =
   let env = Goal.V82.env sigma g in
-  let penv = print_named_context env in
-  let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in
+  let penv = Termops.Internal.print_named_context env in
+  let pc = Termops.Internal.print_constr_env env sigma (Goal.V82.concl sigma g) in
   str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 3456d13bbe..f3581f17dd 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -693,8 +693,9 @@ module Search = struct
           let msg =
             match fst ie with
             | Pretype_errors.PretypeError (env, evd, Pretype_errors.CannotUnify (x,y,_)) ->
-               str"Cannot unify " ++ print_constr_env env evd x ++ str" and " ++
-                                           print_constr_env env evd y
+              str"Cannot unify " ++
+              Printer.pr_econstr_env env evd x ++ str" and " ++
+              Printer.pr_econstr_env env evd y
             | ReachedLimitEx -> str "Proof-search reached its limit."
             | NoApplicableEx -> str "Proof-search failed."
             | e -> CErrors.iprint ie
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 878e2b1f01..596feeec8b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -655,7 +655,7 @@ module New = struct
       | _ ->
 	  let name_elim =
 	    match EConstr.kind sigma elim with
-            | Const _ | Var _ -> str " " ++ print_constr_env (pf_env gl) sigma elim
+            | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim
             | _ -> mt ()
 	  in
 	  user_err ~hdr:"Tacticals.general_elim_then_using"