X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;fp=matitaB%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=ff6f70e946da0ebc17bc78ceff786beef99a0677;hb=04168c737e0916ebdbcdb1457f228bef670c657b;hp=1d3242804a44f280f91ee3c7a50c439b587acae4;hpb=24fc5e5485245fe879e17d46176530b688930b3b;p=helm.git

diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
index 1d3242804..ff6f70e94 100644
--- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
@@ -807,50 +807,42 @@ let disambiguate_term (status: #NCicCoercion.status) ~context ~metasenv ~subst
   let _ = (aliases : GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t) in
   let local_names = List.map (fun (n,_) -> n) context in
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
-   let res,b =
-    MultiPassDisambiguator.disambiguate_thing
-     ~freshen_thing:NotationUtil.freshen_term
-     ~context ~metasenv ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias ~fix_instance
+    Disambiguate.disambiguate_thing
+     ~context ~metasenv ~subst ~use_coercions:true 
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
-     ~universe ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
-     ~passes:(MultiPassDisambiguator.passes ())
-     ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_term
+     ~initial_ugraph:() ~expty
+     ~mk_implicit ~description_of_alias ~fix_instance ~aliases 
+     ~universe ~lookup_in_library 
+     ~uri:None ~pp_thing:(NotationPp.pp_term status) ~pp_term:(NotationPp.pp_term status)
+     ~domain_of_thing:Disambiguate.domain_of_term
      ~interpretate_thing:(interpretate_term status ~obj_context:[] ~mk_choice (?create_dummy_ids:None))
      ~refine_thing:(refine_term status) 
      (text,prefix_len,
       (initialize_ast ~universe ~lookup_in_library ~local_names term))
      ~visit:Disambiguate.bfvisit
-     ~mk_localization_tbl ~expty ~subst
-   in
-    List.map (function (t,a,b,c,_) -> t,a,b,c) res, b
+     ~mk_localization_tbl
 ;;
 
-
 let disambiguate_obj (status: #NCicCoercion.status)
    ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
    ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj) 
  =
   let mk_localization_tbl x = NCicUntrusted.NCicHash.create x in
-   let res,b =
-    let obj' = initialize_obj ~universe ~lookup_in_library obj in
-    MultiPassDisambiguator.disambiguate_thing
-     ~freshen_thing:NotationUtil.freshen_obj
-     ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias ~fix_instance
+  let obj' = initialize_obj ~universe ~lookup_in_library obj in
+    Disambiguate.disambiguate_thing
+     ~context:[] ~metasenv:[] ~subst:[] ~use_coercions:true 
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
-     ~universe 
-     ~uri:(Some uri)
-     ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status)) ~pp_term:(NotationPp.pp_term status)
-     ~passes:(MultiPassDisambiguator.passes ())
-     ~lookup_in_library ~domain_of_thing:Disambiguate.domain_of_obj
+     ~initial_ugraph:() ~expty:None
+     ~mk_implicit ~description_of_alias ~fix_instance ~aliases 
+     ~universe ~lookup_in_library 
+     ~uri:(Some uri) ~pp_thing:(NotationPp.pp_obj (NotationPp.pp_term status))
+     ~pp_term:(NotationPp.pp_term status)
+     ~domain_of_thing:Disambiguate.domain_of_obj
      ~interpretate_thing:(interpretate_obj status ~mk_choice)
      ~refine_thing:(refine_obj status) 
      (text,prefix_len,obj')
      ~visit:Disambiguate.bfvisit_obj
-     ~mk_localization_tbl ~expty:None
-   in
-    List.map (function (o,a,b,c,_) -> o,a,b,c) res, b
+     ~mk_localization_tbl
 ;;
 (*
 let _ =