X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2FmultiPassDisambiguator.ml;h=becf2a41229c18b0b3259a1f2d453a05d0e716c7;hb=84e770b58ae08a345087de816aba29bc2fc727ba;hp=07bbdeba29d68e389590bd3b72650ac1bbe63d2f;hpb=c04f852241510515f06e3bec8eb79acac6e4952e;p=helm.git diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml index 07bbdeba2..becf2a412 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.ml +++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml @@ -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