- Correction d'un bug de coq_makefile sur les variables CAMLLIBS et

  COQLIBS.
- Ajout d'un message d'erreur si Camlp5 est compilé en mode strict




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

3 files changed, 44 insertions, 16 deletions

diff --git a/configure b/configure
index 814e92a55..4ae429f90 100755
--- a/configure
+++ b/configure
@@ -412,6 +412,11 @@ if [ "$camlp5dir" != "" ]; then
 	exit 1
     fi
     camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
+    if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then 
+	echo "Error: Camlp5 found, but in strict mode!"
+	echo "Please compile Camlp5 in transitional mode."
+	exit 1
+    fi
 elif [ "$CAMLTAG" = "OCAML310" ]; then
     if [ -x "${CAMLLIB}/camlp5" ]; then 
         CAMLP4LIB=+camlp5
@@ -424,6 +429,11 @@ elif [ "$CAMLTAG" = "OCAML310" ]; then
     fi
     CAMLP4=camlp5
     camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
+    if [ `$camlp4oexec -pmode 2>&1` = "strict" ]; then 
+	echo "Error: Camlp5 found, but in strict mode!"
+	echo "Please compile Camlp5 in transitional mode."
+	exit 1
+    fi
 else 
     CAMLP4=camlp4
     CAMLP4LIB=+camlp4
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 0599c4982..0dc91af46 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -209,25 +209,43 @@ let is_included dir = function
   | Include dir' -> absolute_dir dir = absolute_dir dir'
   | _ -> false
 
+let dir_of_target t = 
+  match t with
+    | RInclude (dir,_) -> dir
+    | Include dir -> dir
+    | _ -> assert false
+
 let include_dirs l =
+  let rec split_includes l = 
+    match l with
+      | [] -> [], []
+      | Include _ as i :: rem ->
+	  let ri, rr = split_includes rem in 
+	    (i :: ri), rr
+      | RInclude _ as r :: rem -> 
+	  let ri, rr = split_includes rem in 
+	    ri, (r :: rr)
+      | _ :: rem -> split_includes rem
+  in
   let rec parse_includes l = 
     match l with
-      | [] -> [],[]
-      | Include x :: r -> let ri, rr = parse_includes r in
-			    ("-I " ^ x) :: ri, rr
-      | RInclude (p,l) :: r ->
-          let ri, rr = parse_includes r in
+      | [] -> []
+      | Include x :: rem -> ("-I " ^ x) :: parse_includes rem
+      | RInclude (p,l) :: rem ->
 	  let l' = if l = "" then "\"\"" else l in
-            ri, ("-R " ^ p ^ " " ^ l') :: rr
-      | _ :: r -> parse_includes r
+            ("-R " ^ p ^ " " ^ l') :: parse_includes rem
+      | _ :: rem -> parse_includes rem
   in
   let l' = if List.exists (is_included ".") l then l else Include "." :: l in
-  let inc_i, inc_r = parse_includes l' in
-  let inc_i' = List.filter (fun d -> List.exists (fun d' -> is_prefix d' d) inc_r) inc_i in 
+  let inc_i, inc_r = split_includes l' in
+  let inc_i' = List.filter (fun i -> not (List.exists (fun i' -> is_included (dir_of_target i) i') inc_r)) inc_i in 
+  let str_i = parse_includes inc_i in
+  let str_i' = parse_includes inc_i' in
+  let str_r = parse_includes inc_r in
     section "Libraries definition.";
-    print "OCAMLLIBS:="; print_list "\\\n  " inc_i; print "\n";
-    print "COQLIBS:="; print_list "\\\n  " inc_i'; print " "; print_list "\\\n  " inc_r; print "\n";
-    print "COQDOCLIBS:=";   print_list "\\\n  " inc_r; print "\n\n"
+    print "OCAMLLIBS:="; print_list "\\\n  " str_i; print "\n";
+    print "COQLIBS:="; print_list "\\\n  " str_i'; print " "; print_list "\\\n  " str_r; print "\n";
+    print "COQDOCLIBS:=";   print_list "\\\n  " str_r; print "\n\n"
 
 let rec special = function
   | [] -> []
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index ebc939b7e..cca6ac0fc 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -107,10 +107,10 @@ let safe_assoc verbose file k =
 
 let absolute_dir dir =
   let current = Sys.getcwd () in
-  Sys.chdir dir;
-  let dir' = Sys.getcwd () in
-  Sys.chdir current;
-  dir'
+    Sys.chdir dir;
+    let dir' = Sys.getcwd () in
+      Sys.chdir current;
+      dir'
 
 let absolute_file_name basename odir =
   let dir = match odir with Some dir -> dir | None -> "." in