]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/disambiguation/disambiguate.mli
coercions are there, but not heavily tested
[helm.git] / helm / software / components / disambiguation / disambiguate.mli
index cb1882a7d12a900b0e51a39c4e943c32786c623d..5c74b857b49077bd1d68048af460252e5bc023a3 100644 (file)
@@ -123,7 +123,7 @@ val disambiguate_thing:
     '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)