X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=d0bf1ee1751c0ea728d727217d714460cd055445;hb=93ce01455cfeba6b29e3c8a57e28f56559fb891d;hp=0b73296e789da2f2adc7993b930da2f489b075a8;hpb=e6c30351b99a9732c0aa5df361d1510b998afb76;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 0b73296e7..d0bf1ee17 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -443,7 +443,7 @@ sig
       'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
       'raw_thing -> 'ugraph -> localization_tbl:'cichash -> 
         ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
-    localization_tbl:'cichash ->
+    mk_localization_tbl:(int -> 'cichash) ->
     string * int * 'ast_thing ->
     ((DisambiguateTypes.Environment.key * 'alias) list * 
      'metasenv * 'subst * 'refined_thing * 'ugraph)
@@ -459,7 +459,7 @@ let disambiguate_thing
   ~mk_implicit ~description_of_alias
   ~aliases ~universe ~lookup_in_library 
   ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
-  ~localization_tbl
+  ~mk_localization_tbl
   (thing_txt,thing_txt_prefix_len,thing)
 =
   debug_print (lazy "DISAMBIGUATE INPUT");
@@ -533,6 +533,7 @@ let disambiguate_thing
               env in
            aux (aux env l) tl in
       let filled_env = aux aliases todo_dom in
+      let localization_tbl = mk_localization_tbl 503 in
        let cic_thing =
          interpretate_thing ~context ~env:filled_env
           ~uri ~is_path:false thing ~localization_tbl
@@ -636,6 +637,7 @@ in refine_profiler.HExtlib.profile foo ()
                     (inner_dom@remaining_dom@rem_dom) base_univ
                  with
                 | Ok (thing, metasenv,subst,new_univ) ->
+(*                     prerr_endline "OK"; *)
                     let res = 
                       (match inner_dom with
                       | [] ->
@@ -648,6 +650,7 @@ in refine_profiler.HExtlib.profile foo ()
                     in
                      res @@ filter tl
                 | Uncertain loc_msg ->
+(*                     prerr_endline ("UNCERTAIN"); *)
                     let res =
                       (match inner_dom with
                       | [] -> [],[new_env,new_diff,loc_msg],[]
@@ -658,6 +661,7 @@ in refine_profiler.HExtlib.profile foo ()
                     in
                      res @@ filter tl
                 | Ko loc_msg ->
+(*                     prerr_endline "KO"; *)
                     let res = [],[],[new_env,new_diff,loc_msg,true] in
                      res @@ filter tl)
            in