[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.

9 files changed, 29 insertions, 22 deletions

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