Abstraction vis à vis du type loc pour compatibilité ocaml 3.08

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

3 files changed, 12 insertions, 5 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 3522027b9..913f1250d 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -20,6 +20,7 @@ let print_loc loc =
   if loc = dummy_loc then 
     (str"<unknown>")
   else 
+    let loc = unloc loc in
     (int (fst loc) ++ str"-" ++ int (snd loc))
 
 let guill s = "\""^s^"\""
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 012019852..36c3ff3dc 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -103,7 +103,8 @@ let dotted_location (b,e) =
   else 
     (String.make (e-b-1) '.', " ")
 
-let print_highlight_location ib (bp,ep) =
+let print_highlight_location ib loc =
+  let (bp,ep) = unloc loc in
   let bp = bp - ib.start 
   and ep = ep - ib.start in
   let highlight_lines =
@@ -124,7 +125,7 @@ let print_highlight_location ib (bp,ep) =
                       str sn ++ str dn) in 
 	  (l1 ++ li ++ ln)
   in 
-  (str"Toplevel input, characters " ++ Cerrors.print_loc (bp,ep) ++ fnl () ++
+  (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ fnl () ++
      highlight_lines ++ fnl ())
 
 (* Functions to report located errors in a file. *)
@@ -138,6 +139,7 @@ let print_location_in_file s inlibrary fname (bp,ep) =
       (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++
        str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ())
     else
+    let (bp,ep) = unloc (bp,ep) in
     let ic = open_in fname in
     let rec line_of_pos lin bol cnt =
       if cnt < bp then
@@ -151,7 +153,7 @@ let print_location_in_file s inlibrary fname (bp,ep) =
       close_in ic;
       (errstrm  ++ str"File " ++ str ("\""^fname^"\"") ++
          str", line " ++ int line ++
-         str", characters " ++ Cerrors.print_loc (bp-bol,ep-bol) ++ fnl ())
+         str", characters " ++ Cerrors.print_loc (make_loc (bp-bol,ep-bol)) ++ fnl ())
     with e -> (close_in ic; (errstrm ++ str", invalid location." ++ fnl ()))
 	
 let print_command_location ib dloc =
@@ -168,7 +170,8 @@ let valid_loc dloc (b,e) =
     | _ -> true
 	  
 let valid_buffer_loc ib dloc (b,e) =
-  valid_loc dloc (b,e) & b-ib.start >= 0 & e-ib.start < ib.len & b<=e 
+  valid_loc dloc (b,e) & 
+  let (b,e) = unloc (b,e) in b-ib.start >= 0 & e-ib.start < ib.len & b<=e 
 
 (*s The Coq prompt is the name of the focused proof, if any, and "Coq"
     otherwise. We trap all exceptions to prevent the error message printing
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f339159b4..3cc2ba4f8 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -72,6 +72,7 @@ let close_input in_chan (_,verb) =
   with _ -> ()
 
 let verbose_phrase verbch loc =
+  let loc = unloc loc in
   match verbch with
     | Some ch ->
 	let len = snd loc - fst loc in
@@ -131,6 +132,7 @@ let pre_printing = function
 
 let post_printing loc (env,t,f,n) = function
   | VernacSolve (i,_,deftac) ->
+      let loc = unloc loc in
       set_formatter_translator();
       let pp = Ppvernacnew.pr_vernac_solve (i,env,t,deftac) ++ sep_end () in
       (if !translate_file then begin
@@ -142,6 +144,7 @@ let post_printing loc (env,t,f,n) = function
   | _ -> ()
 
 let pr_new_syntax loc ocom =
+  let loc = unloc loc in
   if !translate_file then set_formatter_translator();
   let fs = States.freeze () in
   let com = match ocom with
@@ -255,7 +258,7 @@ and read_vernac_file verbosely s =
     close_input in_chan input;    (* we must close the file first *)
     match real_error e with
       | End_of_input ->
-          if do_translate () then pr_new_syntax (max_int,max_int) None
+          if do_translate () then pr_new_syntax (make_loc (max_int,max_int)) None
       | _ -> raise_with_file fname e
 
 (* raw_do_vernac : char Stream.t -> unit