]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.ml
removed deadcode / fixed typos (thanks to ocaml 3.09)
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml
index ce26f935131f418f26963c4e8121ba7948a74e15..fd8e2a7991e69204ea2a1ec028cea7569460f8ef 100644 (file)
@@ -767,7 +767,6 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
       let todo_dom = domain_diff thing_dom current_dom in
       (* (2) lookup function for any item (Id/Symbol/Num) *)
       let lookup_choices =
-        let id_choices = Hashtbl.create 1023 in
         fun item ->
           let choices =
             let lookup_in_library () =