X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=11d1952050205ba29987690e29c0762be40a933f;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=b9aa8f844fe76a10754a088c2cc2810f3e1d7bd8;hpb=8539d00ff2ed0ffd9b7a08ac8e62376e88987960;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index b9aa8f844..11d195205 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -75,7 +75,7 @@ let refine_term metasenv context uri term ugraph =
           Uncertain,ugraph
       | CicRefine.RefineFailure msg ->
           debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
-            (CicPp.ppterm term) msg);
+            (CicPp.ppterm term) (CicRefine.explain_error msg));
           Ko,ugraph
 
 let refine_obj metasenv context uri obj ugraph =
@@ -91,7 +91,7 @@ let refine_obj metasenv context uri obj ugraph =
          Uncertain,ugraph
      | CicRefine.RefineFailure msg ->
          debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
-           (CicPp.ppobj obj) msg);
+           (CicPp.ppobj obj) (CicRefine.explain_error msg));
          Ko,ugraph
 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =