X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=d3f5b0106cef3868960126c4f75197e16c3525c0;hb=5c3ae2f17d55098676bd50270ddef0bec93618bf;hp=de3701e23401e8cec86445ce5ecbbb4a041a9337;hpb=f5916a7ca7e58c6a3617531e8dbba81d018eb024;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index de3701e23..d3f5b0106 100644
--- 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 = []);