disambiguation takes ~mk_localization_tbl and not ~localization_tbl, thus can

[helm.git] / helm / software / components / cic_disambiguation / cicDisambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index 288be5fa2d5b06fc11a51d4cd682a1b33c1f068c..2b469ce9d7d4b24585421f5007ff1cc80602c1f4 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -642,7 +642,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal
             | _ -> assert false) 
         | k -> k
   in
-  let localization_tbl = Cic.CicHash.create 503 in
+  let mk_localization_tbl x = Cic.CicHash.create x in
    MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
     ~initial_ugraph ~aliases ~string_context_of_context
     ~universe ~lookup_in_library ~mk_implicit ~description_of_alias
@@ -650,7 +650,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal
     ~domain_of_thing:Disambiguate.domain_of_term
     ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
     ~refine_thing:refine_term (text,prefix_len,term)
-    ~localization_tbl
+    ~mk_localization_tbl
     ~hint
     ~freshen_thing:CicNotationUtil.freshen_term
     ~passes:(MultiPassDisambiguator.passes ())
@@ -659,7 +659,7 @@ let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
  ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
 =
   let hint = (fun _ x -> x), fun k -> k in
-  let localization_tbl = Cic.CicHash.create 503 in
+  let mk_localization_tbl x = Cic.CicHash.create x in
   MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] 
     ~aliases ~universe ~uri ~string_context_of_context
     ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
@@ -668,7 +668,7 @@ let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
     ~initial_ugraph:CicUniv.empty_ugraph
     ~interpretate_thing:(interpretate_obj ~mk_choice)
     ~refine_thing:refine_obj
-    ~localization_tbl
+    ~mk_localization_tbl
     ~hint
     ~passes:(MultiPassDisambiguator.passes ())
     ~freshen_thing:CicNotationUtil.freshen_obj