Less verbose error messages (= substitution applied everywhere, terms pretty

[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 de3701e23401e8cec86445ce5ecbbb4a041a9337..d3f5b0106cef3868960126c4f75197e16c3525c0 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -70,11 +70,11 @@ let refine_term metasenv context uri term ugraph =
     with
       | CicRefine.Uncertain msg ->
           debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
-          Uncertain (lazy ("Uncertain trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph
+          Uncertain (lazy ("Uncertain trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)),ugraph
       | CicRefine.RefineFailure msg ->
           debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
             (CicPp.ppterm term) (Lazy.force msg)));
-          Ko (lazy ("Error trying to refine: " ^ CicPp.ppterm term ^ "\n" ^ Lazy.force msg)),ugraph
+          Ko (lazy ("Error trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)),ugraph
 
 let refine_obj metasenv context uri obj ugraph =
  assert (context = []);