From: Stefano Zacchiroli Date: Tue, 13 Sep 2005 13:22:02 +0000 (+0000) Subject: moved dummy_floc from Disambiguate to DisambiguateTypes, since it is now needed by... X-Git-Tag: V_0_1_2_1~27 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=205b08e72f245d4ba210127cf58b1e4b96d5f93a;p=helm.git moved dummy_floc from Disambiguate to DisambiguateTypes, since it is now needed by DisambiguatePp --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 85bdc689c..58927e53b 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -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 diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 10b1c7633..5de2e5759 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -90,5 +90,3 @@ sig CicUniv.universe_graph) list (* disambiguated term *) end -val dummy_floc: Lexing.position * Lexing.position - diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index bb513aa6c..3e969c87a 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -115,3 +115,13 @@ let string_of_domain dom = let empty_environment = Environment.empty +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) + diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index 1a8dc4ac0..df598a3f7 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -96,3 +96,5 @@ type script = CicNotationPt.location * script_entry list val empty_environment: environment +val dummy_floc: Lexing.position * Lexing.position +