This commit (partially) removes a big source of inefficiency (at least for

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index b9aa8f844fe76a10754a088c2cc2810f3e1d7bd8..11d1952050205ba29987690e29c0762be40a933f 100644 (file)
--- 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 = []) () =