From ec339d7f6bcb3442f3aa816addc6a85f6adf5553 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 31 Jan 2005 17:16:41 +0000
Subject: [PATCH] better debug prints

---
 helm/ocaml/cic_disambiguation/disambiguate.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 0ff738fda..aafbeb777 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -35,7 +35,6 @@ exception NoWellTypedInterpretation
 exception Try_again
 
 let debug = false
-let debug = true
 let debug_print = if debug then prerr_endline else ignore
 
 (*
@@ -70,8 +69,11 @@ let refine metasenv context term ugraph =
       | CicRefine.Uncertain _ ->
           debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
           Uncertain,ugraph
-      | CicRefine.RefineFailure _ ->
-          debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
+      | CicRefine.RefineFailure msg ->
+          debug_print (
+            (sprintf ("%%%%%% PRUNED!!!\n<<begin cause>>\n" ^^ 
+              "%s\n<<end cause>>\n<<begin term>>\n%s\n<<end term>>") 
+              msg (CicPp.ppterm term)));
           Ko,ugraph
       | CicUnification.UnificationFailure s -> 
 	 prerr_endline ("PASSADI QUI: " ^ s);
-- 
2.39.2