From 081cb0ae54c7e5babdedeea7559d667183a38638 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 22 Nov 2005 09:52:32 +0000 Subject: [PATCH] Debugging code commented out. --- helm/ocaml/cic_unification/cicRefine.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 202fa8cd7..d3a297d43 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -1116,15 +1116,16 @@ and type_of_aux' metasenv context t ugraph = match coer with | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> - let msg = + let msg e = lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst hete context ^ " has type " ^ CicMetaSubst.ppterm_in_context subst hety context ^ " but is here used with type " ^ - CicMetaSubst.ppterm_in_context subst s context) + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)) in - enrich (fun _ -> msg) exn + enrich msg exn | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy "Coercions on meta")) | CoercGraph.SomeCoercion c -> -- 2.39.2