From a3bc73ee710387e84d1cd33a3f8f6303daa7cc1f Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 1 Feb 2005 17:55:29 +0000
Subject: [PATCH] enriched error message

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

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 67b6d115c..9f4c41d2e 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -67,13 +67,11 @@ let refine metasenv context term ugraph =
 	(Ok (term', metasenv')),ugraph1
     with
       | CicRefine.Uncertain _ ->
-          debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ;
+          debug_print ("UNCERTAIN!!! " ^ CicPp.ppterm term) ;
           Uncertain,ugraph
       | 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)));
+          debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+            (CicPp.ppterm term) msg);
           Ko,ugraph
       | CicUnification.UnificationFailure s -> 
 	 prerr_endline ("PASSADI QUI: " ^ s);
-- 
2.39.2