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/unification.ml | |
| parent | 523c5e41f78dbd4dfbb60d4d7c78f01a22b30aa2 (diff) | |
| parent | 7628af7af9ff20d2a894673f66c3753e214623f1 (diff) | |
Merge PR #6524: [print] Restrict use of "debug" Termops printer.
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 6 |
1 files changed, 4 insertions, 2 deletions
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 |