From 7628af7af9ff20d2a894673f66c3753e214623f1 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 29 Dec 2017 20:20:38 +0100 Subject: [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. --- pretyping/evarconv.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'pretyping/evarconv.ml') 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 -- cgit v1.2.3