X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcic_disambiguation%2Fdisambiguate.ml;h=1d4a6a61ef9ecd8a1cbf8613035014c768fc568c;hb=df70518efb295cdce60a3df8098ac0a6eef2d9cf;hp=9dc19c7c6a3b281056d4c0c9c640b41d58217a43;hpb=76c2d13b7641cdffae2759b511cbecbd91afa14e;p=helm.git

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 9dc19c7c6..1d4a6a61e 100644
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -838,7 +838,7 @@ sig
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
-    CicNotationPt.obj disambiguator_input ->
+    CicNotationPt.term CicNotationPt.obj disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
@@ -1204,7 +1204,7 @@ in refine_profiler.HExtlib.profile foo ()
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
       in
       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
-        ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj
+        ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj
         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
         (text,prefix_len,obj)
   end