Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -rectypes)

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

7 files changed, 23 insertions, 22 deletions

diff --git a/config/Makefile.template b/config/Makefile.template
index d4fa11783..6161089ae 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -65,7 +65,7 @@ CAMLOPTLINK="NATIVECAMLC"
 CAMLMKTOP="CAMLMKTOPEXEC"
 
 # Caml flags
-CAMLFLAGS=CAMLANNOTATEFLAG
+CAMLFLAGS=-rectypes CAMLANNOTATEFLAG
 
 # Compilation debug flag
 CAMLDEBUG=COQDEBUGFLAG
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 65439dd26..9b257014e 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -95,9 +95,9 @@ let pr_patnotation = pr_notation_gen decode_patlist_value
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
-let pr_located pr ((b,e),x) =
-  if Options.do_translate() && (b,e)<>dummy_loc then
-    let (b,e) = unloc (b,e) in
+let pr_located pr (loc,x) =
+  if Options.do_translate() && loc<>dummy_loc then
+    let (b,e) = unloc loc in
     comment b ++ pr x ++ comment e
   else pr x
 
@@ -142,7 +142,7 @@ let pr_opt_type_spc pr = function
   | CHole _ -> mt ()
   | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
-let pr_lident (b,_ as loc,id) =
+let pr_lident (loc,id) =
   if loc <> dummy_loc then
     let (b,_) = unloc loc in
     pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 668cfe6f3..d44e225b5 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -28,7 +28,7 @@ open Tacinterp
 
 let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
 
-let pr_lident (b,_ as loc,id) =
+let pr_lident (loc,id) =
   if loc <> dummy_loc then
     let (b,_) = unloc loc in
     pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id)
@@ -39,7 +39,7 @@ let string_of_fqid fqid =
 
 let pr_fqid fqid = str (string_of_fqid fqid)
 
-let pr_lfqid (_,_ as loc,fqid) =
+let pr_lfqid (loc,fqid) =
   if loc <> dummy_loc then
    let (b,_) = unloc loc in
     pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid)
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 7c684cdc1..513d345b5 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -39,18 +39,18 @@ let mlexpr_of_list f l =
   List.fold_right
     (fun e1 e2 ->
       let e1 = f e1 in
-       let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
+       let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
        <:expr< [$e1$ :: $e2$] >>)
     l (let loc = dummy_loc in <:expr< [] >>)
 
 let mlexpr_of_pair m1 m2 (a1,a2) =
   let e1 = m1 a1 and e2 = m2 a2 in
-  let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in
+  let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in
   <:expr< ($e1$, $e2$) >>
 
 let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)=
   let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in
-  let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e3)) in
+  let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in
   <:expr< ($e1$, $e2$, $e3$) >>
 
 (* We don't give location for tactic quotation! *)
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 476732a3f..6e8425d98 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -10,12 +10,12 @@
 
 (* $Id$ *)
 
+open Util
 open Genarg
 open Q_util
 open Q_coqast
 open Argextend
 
-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
 let loc = Util.dummy_loc
 let default_loc = <:expr< Util.dummy_loc >>
 
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 3c8526c08..0b3dd75ad 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -10,12 +10,12 @@
 
 (* $Id$ *)
 
+open Util
 open Genarg
 open Q_util
 open Q_coqast
 open Argextend
 
-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
 let loc = Util.dummy_loc
 let default_loc = <:expr< Util.dummy_loc >>
 
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 7f21de041..fbdc96d6e 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -139,16 +139,16 @@ let print_highlight_location ib loc =
 
 (* Functions to report located errors in a file. *)
 
-let print_location_in_file s inlibrary fname (bp,ep) =
+let print_location_in_file s inlibrary fname loc =
   let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in
-  if (bp,ep) = dummy_loc then 
+  if loc = dummy_loc then 
     (errstrm ++ str", unknown location." ++ fnl ())
   else
     if inlibrary then
       (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++
-       str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ())
+       str" characters " ++ Cerrors.print_loc loc ++ fnl ())
     else
-    let (bp,ep) = unloc (bp,ep) in
+    let (bp,ep) = unloc loc in
     let ic = open_in fname in
     let rec line_of_pos lin bol cnt =
       if cnt < bp then
@@ -172,15 +172,16 @@ let print_command_location ib dloc =
            str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ())
     | None -> (mt ())
 
-let valid_loc dloc (b,e) =
-  (b,e) <> dummy_loc
+let valid_loc dloc loc =
+  loc <> dummy_loc
   & match dloc with
-    | Some (bd,ed) -> bd<=b & e<=ed
+    | Some dloc ->
+	let (bd,ed) = unloc dloc in let (b,e) = unloc loc in bd<=b & e<=ed
     | _ -> true
 	  
-let valid_buffer_loc ib dloc (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 
+let valid_buffer_loc ib dloc loc =
+  valid_loc dloc loc & 
+  let (b,e) = unloc loc 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