Abstraction vis a vis du type loc pour ocaml 3.08

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5951 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 6 insertions, 6 deletions

diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
index 17bd6ef4e1..67279bb828 100644
--- a/contrib/interface/ctast.ml
+++ b/contrib/interface/ctast.ml
@@ -3,7 +3,7 @@
 open Names
 open Libnames
 
-type loc = int * int
+type loc = Util.loc
 
 type t =
   | Node of loc * string * t list
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index a391abf33c..ec98929604 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -49,7 +49,7 @@ type dad_rule =
 
 (* This value will be used systematically when constructing objects *)
 
-let zz = (0,0);;
+let zz = Util.dummy_loc;;
 
 (* This function receives a length n, a path p, and a term and returns a
    couple whose first component is the subterm designated by the prefix
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index e8f6a56ee0..e0f88ba69a 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -22,7 +22,7 @@ open Genarg;;
 open Topconstr;;
 open Termops;;
 
-let zz = (0,0);;
+let zz = Util.dummy_loc;;
 
 let hyp_radix = id_of_string "H";;
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ce44196d86..d2562e9781 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -65,7 +65,7 @@ let set_coercion_description f =
  coercion_description_holder:=f; ();;
 
 let string_of_node_loc the_node =
-  match loc the_node with
+  match unloc (loc the_node) with
       (a,b) -> "(" ^ (string_of_int a) ^ ", " ^ (string_of_int b) ^ ")";;
 
 let xlate_error s = failwith ("Translation error: " ^ s);;
diff --git a/ide/coq.mli b/ide/coq.mli
index 6c4608c5cb..5e2c44de47 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -36,7 +36,7 @@ val get_current_goals_nb : unit -> int
 
 val print_no_goal : unit -> string
 
-val process_exn : exn -> string*((int*int) option)
+val process_exn : exn -> string*(Util.loc option)
 
 type reset_info = NoReset | Reset of Names.identifier * bool ref
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 5922f1edb5..bfbee58cad 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -974,7 +974,7 @@ object(self)
 	 self#set_message s;
 	 message_view#misc#draw None;
 	 if localize then 
-	   (match loc with 
+	   (match Util.option_app Util.unloc loc with 
 	    | None -> ()
 	    | Some (start,stop) ->
 		let convert_pos = byte_offset_to_char_offset phrase in