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

10 files changed, 34 insertions, 20 deletions

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 596413660..4bc0c6fa2 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -9,6 +9,7 @@
 (*i $Id$ *)
 
 (*i*)
+open Util
 open Names
 open Term
 open Termops
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6c0febecf..9217400bc 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -155,10 +155,11 @@ let add_glob loc ref =
   let sp = Nametab.sp_of_global ref in
   let id = let _,id = repr_path sp in string_of_id id in
   let dp = string_of_dirpath (Lib.library_part ref) in
-  dump_string (Printf.sprintf "R%d %s.%s\n" (fst loc) dp id)
+  dump_string (Printf.sprintf "R%d %s.%s\n" (fst (unloc loc)) dp id)
 
 let loc_of_notation f loc args ntn =
-  if args=[] or ntn.[0] <> '_' then fst loc else snd (f (List.hd args))
+  if args=[] or ntn.[0] <> '_' then fst (unloc loc)
+  else snd (unloc (f (List.hd args)))
 
 let ntn_loc = loc_of_notation constr_loc
 let patntn_loc = loc_of_notation cases_pattern_loc
@@ -166,7 +167,8 @@ let patntn_loc = loc_of_notation cases_pattern_loc
 let dump_notation_location =
   fun pos ntn ((path,df),sc) ->
     let rec next growing =
-      let (bp,_ as loc) = Lexer.location_function !token_number in
+      let loc = Lexer.location_function !token_number in
+      let (bp,_) = unloc loc in
       if growing then if bp >= pos then loc else (incr token_number;next true)
       else if bp = pos then loc
       else if bp > pos then (decr token_number;next false)
@@ -175,7 +177,7 @@ let dump_notation_location =
     last_pos := pos;
     let path = string_of_dirpath path in
     let sc = match sc with Some sc -> " "^sc | None -> "" in
-    dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst loc) path df sc)
+    dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst (unloc loc)) path df sc)
 
 (**********************************************************************)
 (* Contracting "{ _ }" in notations *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0a9347360..b65365458 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -31,6 +31,7 @@ let thm_token = G_proofs.thm_token
 (* compilation on PowerPC and Sun architectures *)
 
 let filter_com (b,e) =
+  let (b,e) = unloc (b,e) in
   Pp.comments := List.filter (fun ((b',e'),s) -> b'<b || e'>e) !Pp.comments 
 
 if !Options.v7 then
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 63aecdcb4..c016d86f7 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -147,7 +147,7 @@ let init () =
 let _ = init()
 
 (* Errors occuring while lexing (explained as "Lexer error: ...") *)
-let err loc str = Stdpp.raise_with_loc loc (Error str)
+let err loc str = Stdpp.raise_with_loc (Util.make_loc loc) (Error str)
 
 (* The string buffering machinery *)
 
@@ -480,7 +480,7 @@ let loct_func loct i =
     else if !loct.(i/tsz) = [| |] then None
     else !loct.(i/tsz).(i mod tsz)
   with
-    | Some loc -> loc
+    | Some loc -> Util.make_loc loc
     | _ -> locerr ()
 
 let loct_add loct i loc =
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a54754e7d..f9c8d5329 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -8,12 +8,11 @@
 
 (* $Id$ *)
 
+open Util
 open Names
 open Libnames
 open Q_util
 
-let dummy_loc = (0,0)
-
 let is_meta s = String.length s > 0 && s.[0] == '$'
 
 let purge_str s =
@@ -22,7 +21,8 @@ let purge_str s =
 
 let anti loc x =
   let e =
-    let loc = (1, snd loc - fst loc) in <:expr< $lid:purge_str x$ >>
+    let loc = unloc loc in
+    let loc = make_loc (1, snd loc - fst loc) in <:expr< $lid:purge_str x$ >>
   in
   <:expr< $anti:e$ >>
 
@@ -110,7 +110,7 @@ and expr_list_of_var_list sl =
 (* We don't give location for tactic quotation! *)
 let loc = dummy_loc
 
-let dloc = <:expr< (0,0) >>
+let dloc = <:expr< Util.dummy_loc >>
 
 let mlexpr_of_ident id =
   <:expr< Names.id_of_string $str:Names.string_of_id id$ >>
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
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 6bac9b1f1..47a92f7ca 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -96,6 +96,7 @@ let surround p = hov 1 (str"(" ++ p ++ str")")
 
 let pr_located pr ((b,e),x) =
   if Options.do_translate() && (b,e)<>dummy_loc then
+    let (b,e) = unloc (b,e) in
     comment b ++ pr x ++ comment e
   else pr x
 
@@ -146,7 +147,8 @@ let pr_name = function
 
 let pr_lident (b,_ as loc,id) =
   if loc <> dummy_loc then
-    pr_located pr_id ((b,b+String.length(string_of_id id)),id)
+    let (b,_) = unloc loc in
+    pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
   else pr_id id
 
 let pr_lname = function
@@ -189,8 +191,8 @@ let pr_eqn pr (loc,pl,rhs) =
       pr_sep_com spc (pr ltop) rhs))
 
 let begin_of_binder = function
-    LocalRawDef(((b,_),_),_) -> b
-  | LocalRawAssum(((b,_),_)::_,_) -> b
+    LocalRawDef((loc,_),_) -> fst (unloc loc)
+  | LocalRawAssum((loc,_)::_,_) -> fst (unloc loc)
   | _ -> assert false
 
 let begin_of_binders = function
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index e0354caf2..b7e739a5c 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -32,7 +32,8 @@ let pr_spc_type = pr_sep_com spc pr_type
 
 let pr_lident (b,_ as loc,id) =
   if loc <> dummy_loc then
-    pr_located pr_id ((b,b+String.length(string_of_id id)),id)
+    let (b,_) = unloc loc in
+    pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
   else pr_id id
 
 let pr_lname = function
@@ -313,7 +314,7 @@ let pr_onescheme (id,dep,ind,s) =
 
 let begin_of_inductive = function
     [] -> 0
-  | (_,(((b,_),_),_))::_ -> b
+  | (_,((loc,_),_))::_ -> fst (unloc loc)
 
 let pr_class_rawexpr = function
   | FunClass -> str"Funclass"