From 420f78b2caeaaddc6fe484565b2d0e49c66888e5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 27 Jul 2014 10:02:38 +0200 Subject: Imported Upstream version 8.4pl4dfsg --- pretyping/evarconv.ml | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f0019448..8b421ea3 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* !debug_unification); + Goptions.optwrite = (fun a -> debug_unification:=a); +} + + type flex_kind_of_term = | Rigid of constr | PseudoRigid of constr (* approximated as rigid but not necessarily so *) @@ -210,6 +221,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) in (* Evar must be undefined since we have flushed evars *) + let () = if !debug_unification then + let open Pp in + let pr_state (tm,l) = + h 0 (Termops.print_constr tm ++ str "|" ++ cut () + ++ prlist_with_sep pr_semicolon + (fun x -> hov 1 (Termops.print_constr x)) l) in + pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> let f1 i = -- cgit v1.2.3