From 205b08e72f245d4ba210127cf58b1e4b96d5f93a Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 13 Sep 2005 13:22:02 +0000
Subject: [PATCH] moved dummy_floc from Disambiguate to DisambiguateTypes,
 since it is now needed by DisambiguatePp

---
 helm/ocaml/cic_disambiguation/disambiguate.ml       | 10 ----------
 helm/ocaml/cic_disambiguation/disambiguate.mli      |  2 --
 helm/ocaml/cic_disambiguation/disambiguateTypes.ml  | 10 ++++++++++
 helm/ocaml/cic_disambiguation/disambiguateTypes.mli |  2 ++
 4 files changed, 12 insertions(+), 12 deletions(-)

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
+
-- 
2.39.2