From 7abc521440f9002e61ce66b25a4150f41e5a813b Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Mon, 3 Feb 2014 10:28:06 +0100 Subject: Create Debug Unification option to dump states that Evarconv.eq_appr_x tries to unify. --- pretyping/evarconv.ml | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 035cebb94..59dac7322 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -23,6 +23,17 @@ open Globnames open Evd open Pretype_errors +let debug_unification = ref (false) +let _ = Goptions.declare_bool_option { + Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optname = + "Print states sended to Evarconv unification"; + Goptions.optkey = ["Debug";"Unification"]; + Goptions.optread = (fun () -> !debug_unification); + Goptions.optwrite = (fun a -> debug_unification:=a); +} + + type flex_kind_of_term = | Rigid | MaybeFlexible (* approx'ed as reducible but not necessarily so *) @@ -312,6 +323,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) + let () = if !debug_unification then + let open Pp in + pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in match (flex_kind_of_term term1 sk1, flex_kind_of_term term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> let f1 i = -- cgit v1.2.3