Coq should compile with Ocaml4 and/or lablgtk installed with ocamlfind

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

2 files changed, 14 insertions, 9 deletions

diff --git a/configure b/configure
index 072d4d2ee..bc80f0123 100755
--- a/configure
+++ b/configure
@@ -471,7 +471,7 @@ case $CAMLVERSION in
 	    echo "          Configuration script failed!"
 	    exit 1
 	fi;;
-    3.11.2|3.12*)
+    3.11.2|3.12*|4.*)
 	CAMLP4COMPAT="-loc loc" 
 	echo "You have Objective-Caml $CAMLVERSION. Good!";;
     *)
@@ -494,7 +494,7 @@ esac
 
 if [ "$coq_debug_flag" = "-g" ]; then
     case $CAMLTAG in
-        OCAML31*)
+        OCAML31*|OCAML4*)
             # Compilation debug flag
             coq_debug_flag_opt="-g"
             ;;
@@ -568,7 +568,7 @@ case $usecamlp5 in
   yes)
     camlp4oexec=`echo "$camlp4oexec" | tr 4 5`
     case `"$camlp4oexec" -v 2>&1` in
-	*4.0*|*5.00*)
+	*"version 4.0"*|*5.00*)
 	    echo "Camlp5 version < 5.01 not supported."
 	    echo "Configuration script failed!"
 	    exit 1;;
@@ -654,11 +654,11 @@ if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then
     echo "CoqIde disabled as requested."
 else
     case $lablgtkdir_spec in
-	no) 
-	    if [ -f "${CAMLLIB}/lablgtk2/gSourceView2.mli" ]; then
+	no)
+            if lablgtkdir=$(ocamlfind query lablgtk2.sourceview2 2> /dev/null); then
+                lablgtkdir_spec=yes
+	    elif [ -f "${CAMLLIB}/lablgtk2/gSourceView2.mli" ]; then
 		lablgtkdir=${CAMLLIB}/lablgtk2
-	    elif [ -f "${CAMLLIB}/site-lib/lablgtk2/gSourceView2.mli" ]; then
-		lablgtkdir=${CAMLLIB}/site-lib/lablgtk2
 	    fi;;
 	yes)
 	    if [ ! -f "$lablgtkdir/gSourceView2.mli" ]; then
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 55e12a30e..bd4dec2b6 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -52,6 +52,8 @@ let top        = ref false
 let echo       = ref false
 let no_start   = ref false
 
+let is_ocaml4 = String.sub Coq_config.caml_version 0 2 = "4."
+
 let src_dirs () =
   [ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ]
 
@@ -62,7 +64,8 @@ let includes () =
       (fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l)
       (src_dirs ())
       (["-I"; "\"" ^ camlp4lib ^ "\""] @
-	  ["-I"; "\"" ^ coqlib ^ "\""])
+	  ["-I"; "\"" ^ coqlib ^ "\""] @
+         if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
 
 (* Transform bytecode object file names in native object file names *)
 let native_suffix f =
@@ -261,7 +264,9 @@ let main () =
         ocamloptexec^" -linkall"
     end else
       (* bytecode (we shunt ocamlmktop script which fails on win32) *)
-      let ocamlmktoplib = " toplevellib.cma" in
+      let ocamlmktoplib = if is_ocaml4
+	then " ocamlcommon.cma ocamlbytecomp.cma ocamltoplevel.cma"
+	else " toplevellib.cma" in
       let ocamlcexec = Filename.concat camlbin "ocamlc" in
       let ocamlccustom = Printf.sprintf "%s %s -linkall "
         ocamlcexec Coq_config.coqrunbyteflags in