diff options
| author | Pierre-Marie Pédrot | 2018-09-27 14:11:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-27 14:11:36 +0200 |
| commit | 64a8f3cbb2fa278ed9d7bf2e5567d4e2b9bfa9dc (patch) | |
| tree | 3171d8632e1dd95072c93b76a9627d4c0363ae96 /pretyping/evarconv.ml | |
| parent | 523c5e41f78dbd4dfbb60d4d7c78f01a22b30aa2 (diff) | |
| parent | 7628af7af9ff20d2a894673f66c3753e214623f1 (diff) | |
Merge PR #6524: [print] Restrict use of "debug" Termops printer.
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 7 |
1 files changed, 4 insertions, 3 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 |