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

2 files changed, 23 insertions, 8 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)