diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-17 09:06:09 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-17 09:06:09 +0100 |
| commit | ac3ee8cba2d27f2be38ba706e49aeee08086d936 (patch) | |
| tree | 67c2633ac657abd1b5bc2a26b27b7cb7a9aad868 | |
| parent | f2bbdd31a6aa62d8a000f5a91f666e68e7241964 (diff) | |
| parent | 105f346cc707b3433379514cd5ddcd3389912083 (diff) | |
Merge PR#437: Improve unification debug trace.
| -rw-r--r-- | pretyping/evarconv.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a2ffe12e9..88ea08c84 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -500,8 +500,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 ()) - ++ fnl ()) in + Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state 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) -> @@ -1129,6 +1128,10 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp 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 let app_empty = Array.is_empty l1 && Array.is_empty l2 in match kind_of_term term1, kind_of_term term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty |