X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=c34a5731505c0b9b38d10b11ad91ab1ca9387ce7;hb=4112b9f87a555bfc4c3cd06bae652cd2382cad8b;hp=95ee85c243db9ff4731941611a114ac909d47782;hpb=acf77bb24694158a57444c7f32da46ceac8b30c4;p=helm.git

diff --git a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
index 95ee85c24..c34a57315 100644
--- a/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/nCicDisambiguate.ml
@@ -18,8 +18,8 @@ open DisambiguateTypes
 module Ast = NotationPt
 module NRef = NReference 
 
-let debug_print s = prerr_endline (Lazy.force s);;
-(* let debug_print _ = ();; *)
+(*let debug_print s = prerr_endline (Lazy.force s);;*)
+let debug_print _ = ();;
 
 let cic_name_of_name = function
   | Ast.Ident (n,_) ->  n
@@ -654,8 +654,8 @@ let rec initialize_ast (* ~aliases *) ~universe ~lookup_in_library ~local_names
                | DisambiguateTypes.Symbol _ -> "SYM"
                | DisambiguateTypes.Num _ -> "NUM"
              in
-             prerr_endline (Printf.sprintf "lookup_choices of %s returns length %d" id
-               (List.length res));
+             debug_print (lazy (Printf.sprintf "lookup_choices of %s returns length %d" id
+               (List.length res)));
              res
           with Not_found -> [])
    in
@@ -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 _ =