Merge PR #6524: [print] Restrict use of "debug" Termops printer.

2 files changed, 37 insertions, 6 deletions

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"]