]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/disambiguation/multiPassDisambiguator.ml
added empty_db, usefull to avoid translating all old coercions to obtain a new coerci...
[helm.git] / helm / software / components / disambiguation / multiPassDisambiguator.ml
index 07bbdeba29d68e389590bd3b72650ac1bbe63d2f..becf2a41229c18b0b3259a1f2d453a05d0e716c7 100644 (file)
@@ -142,16 +142,15 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
 let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
   ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit
   ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing
-  ~domain_of_thing ~interpretate_thing ~refine_thing ~localization_tbl thing
+  ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl thing
  =
   let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
-    let thing = if fresh_instances then freshen_thing thing else thing
-    in
+    let thing = if fresh_instances then freshen_thing thing else thing in
      Disambiguate.disambiguate_thing
       ~context ~metasenv ~subst ~use_coercions ~string_context_of_context
       ~initial_ugraph ~hint ~mk_implicit ~description_of_alias
       ~aliases ~universe ~lookup_in_library 
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
-      ~localization_tbl (txt,len,thing)
+      ~mk_localization_tbl (txt,len,thing)
   in
   disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing