X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=58927e53b887d8b7aeddfe9e82c4a6e85a7bbc7b;hb=86eaff4471bdce9f632838d3a0b18d082015c2db;hp=919c33eb76526e31035e13721ae25e6caffb7845;hpb=35c68efd0a44da26d4aa6ae760ee03712b33dfed;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 919c33eb7..58927e53b 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -37,7 +37,7 @@ exception Try_again type aliases = bool * DisambiguateTypes.environment -let debug = true +let debug = false let debug_print = if debug then prerr_endline else ignore (* @@ -49,16 +49,6 @@ let domain_size = ref 0 let choices_avg = ref 0. *) -let floc_of_loc (loc_begin, loc_end) = - let floc_begin = - { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1; - Lexing.pos_cnum = loc_begin } - in - let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in - (floc_begin, floc_end) - -let dummy_floc = floc_of_loc (-1, -1) - let descr_of_domain_item = function | Id s -> s | Symbol (s, _) -> s