Discontinue support for ocaml 3.09.*

Ocaml 3.10.0 is already three year old...

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

9 files changed, 25 insertions, 107 deletions

diff --git a/INSTALL b/INSTALL
index 7b022f534..e88dc3199 100644
--- a/INSTALL
+++ b/INSTALL
@@ -41,12 +41,10 @@ WHAT DO YOU NEED ?
 
    Should you need or prefer to compile Coq V8.2 yourself, you need:
 
-     - Objective Caml version 3.09.3 or later
+     - Objective Caml version 3.10.0 or later
        (available at http://caml.inria.fr/)
 
-       For Ocaml version >= 3.10.0, you also need to install camlp5
-       (version <= 4.08, or 5.01 transitional)
-  
+     - Camlp5 (version <= 4.08, or 5.* transitional)
 
      - GNU Make version 3.81 or later
        (
@@ -89,7 +87,7 @@ QUICK INSTALLATION PROCEDURE.
 INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 =================================================
 
-1- Check that you have the Objective Caml compiler version 3.09.3 (or later)
+1- Check that you have the Objective Caml compiler version 3.10.0 (or later)
    installed on your computer and that "ocamlmktop" and "ocamlc" (or
    its native code version "ocamlc.opt") lie in a directory which is present
    in your $PATH environment variable. 
diff --git a/INSTALL.ide b/INSTALL.ide
index 757d83548..d09df2eb0 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -23,7 +23,7 @@ On Gentoo GNU/Linux, do:
 Else, read the rest of this document to compile your own CoqIde.
 
 REQUIREMENT:
-	- OCaml >= 3.09.3 with native threads support.
+	- OCaml >= 3.10 with native threads support.
 	- make world must succeed.
 	- The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
 	  The official supported version is at least 2.8.x.
diff --git a/README.win b/README.win
index 7e0d21105..9f6eff799 100644
--- a/README.win
+++ b/README.win
@@ -20,7 +20,7 @@ COMPILATION.
     distribution. If you really need to recompile under Windows, here
     are some indications:
 
-    1- Install ocaml for Windows (MinGW port), preferably version 3.09.3.
+    1- Install ocaml for Windows (MinGW port).
        See: http://caml.inria.fr
 
     2- Install a shell environment with at least:
diff --git a/configure b/configure
index 5ad950260..69a900b3b 100755
--- a/configure
+++ b/configure
@@ -420,16 +420,16 @@ esac
 CAMLVERSION=`"$bytecamlc" -version`
 
 case $CAMLVERSION in
-    1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09.[012])
+    1.*|2.*|3.0*)
 	echo "Your version of Objective-Caml is $CAMLVERSION."
 	if [ "$force_caml_version" = "yes" ]; then
 	    echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml."
 	else
-	    echo "          You need Objective-Caml 3.09.3 or later."
+	    echo "          You need Objective-Caml 3.10.0 or later."
 	    echo "          Configuration script failed!"
 	    exit 1
 	fi;;
-    ?*)
+    3.1*)
 	CAMLP4COMPAT="-loc loc" 
 	echo "You have Objective-Caml $CAMLVERSION. Good!";;
     *)
@@ -450,12 +450,6 @@ case $ARCH in
       CAMLLIB=`"$CAMLC" -where`
 esac
 
-# We need to set a special flag for OCaml 3.07
-case  $CAMLVERSION in 
-	3.07*)
-	  cflags="$cflags -DOCAML_307";;
-esac
-
 if [ "$coq_debug_flag" = "-g" ]; then
     case $CAMLTAG in
         OCAML31*)
@@ -547,14 +541,7 @@ CAMLP4BIN=${CAMLBIN}
 if [ "$best_compiler" = "opt" ] ; then
   if test -e "$nativecamlc" || test -e "`which $nativecamlc`"; then
       CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
-      if [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then
-	  case $CAMLOPTVERSION in
-	      3.09.3|3.1?*) ;;
-	      *) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3,"
-		 best_compiler=byte
-		 echo "only the bytecode version of Coq will be available."
-	  esac
-      elif [ ! -f $FULLCAMLP4LIB/gramlib.cmxa ]; then
+      if [ ! -f $FULLCAMLP4LIB/gramlib.cmxa ]; then
 	  best_compiler=byte
 	  echo "Cannot find native-code $CAMLP4,"
 	  echo "only the bytecode version of Coq will be available."
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 98ef27911..a45183f30 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -80,13 +80,6 @@ sp is a local copy of the global variable extern_sp. */
 #   define print_int(i) 
 #endif
 
-/* Wrapper pour caml_modify */ 	 
-#ifdef OCAML_307 	 
-#define CAML_MODIFY(a,b) modify(a,b) 	 
-#else 	 
-#define CAML_MODIFY(a,b) caml_modify(a,b) 	 
-#endif
-
 /* GC interface */
 #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; }
 #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; }
@@ -659,7 +652,7 @@ value coq_interprete
 	  Field(accu, 0) = sp[0];
 	  *sp = accu;
 	  /* mise a jour du block accumulate */
-	  CAML_MODIFY(&Field(p[i], 1),*sp);
+	  caml_modify(&Field(p[i], 1),*sp);
 	  sp++;
 	}
 	pc += nfunc;
@@ -830,7 +823,7 @@ value coq_interprete
       
       Instruct(SETFIELD0){
 	print_instr("SETFIELD0");
-	CAML_MODIFY(&Field(accu, 0),*sp);
+	caml_modify(&Field(accu, 0),*sp);
 	sp++;
 	Next;
       }
@@ -838,7 +831,7 @@ value coq_interprete
       Instruct(SETFIELD1){
         int i, j, size, size_aux;
 	print_instr("SETFIELD1");
-	CAML_MODIFY(&Field(accu, 1),*sp);
+	caml_modify(&Field(accu, 1),*sp);
        	sp++;
 	Next; 
       }
@@ -856,9 +849,9 @@ value coq_interprete
 	    *sp = accu;
 	    Alloc_small(accu, 1, ATOM_COFIX_TAG);
 	    Field(accu, 0) = Field(Field(*sp, 1), 0);
-	    CAML_MODIFY(&Field(*sp, 1), accu);
+	    caml_modify(&Field(*sp, 1), accu);
 	    accu = *sp; sp++;
-            CAML_MODIFY(&Field(*sp, i), accu);
+            caml_modify(&Field(*sp, i), accu);
 	  }
 	}
 	sp++;
@@ -867,7 +860,7 @@ value coq_interprete
       
       Instruct(SETFIELD){
 	print_instr("SETFIELD");
-	CAML_MODIFY(&Field(accu, *pc),*sp);
+	caml_modify(&Field(accu, *pc),*sp);
 	sp++; pc++;
 	Next;
       }	
diff --git a/lib/compat.ml4 b/lib/compat.ml4
index 7566624b8..4ec4d915c 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -10,10 +10,8 @@
 
 (* Compatibility file depending on ocaml version *)
 
-IFDEF OCAML309 THEN DEFINE OCAML308 END
-
 IFDEF CAMLP5 THEN
-module M = struct
+
 type loc = Stdpp.location
 let dummy_loc = Stdpp.dummy_loc
 let make_loc = Stdpp.make_loc
@@ -23,45 +21,9 @@ let join_loc loc1 loc2 =
  else Stdpp.encl_loc loc1 loc2
 type token = string*string
 type lexer = token Token.glexer
-end
-ELSE IFDEF OCAML308 THEN
-module M = struct
-type loc = Token.flocation
-let dummy_loc = Token.dummy_loc
-let make_loc loc = Token.make_loc loc
-let unloc (b,e) =
-  let loc = (b.Lexing.pos_cnum,e.Lexing.pos_cnum) in
-  (* Ensure that we unpack a char location that was encoded as a line-col
-     location by make_loc *)
-(* Gram.Entry.parse may send bad loc in 3.08, see caml-bugs #2954
-  assert (dummy_loc = (b,e) or make_loc loc = (b,e));
-*)
-  loc
-let join_loc loc1 loc2 =
- if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
- else (fst loc1, snd loc2)
-type token = Token.t
-type lexer = Token.lexer
-end
-ELSE
-module M = struct
-type loc = int * int
-let dummy_loc = (0,0)
-let make_loc x = x
-let unloc x = x
-let join_loc loc1 loc2 =
- if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc
- else (fst loc1, snd loc2)
-type token = Token.t
-type lexer = Token.lexer
-end
-END
-END
 
-type loc = M.loc
-let dummy_loc = M.dummy_loc
-let make_loc = M.make_loc
-let unloc = M.unloc
-let join_loc = M.join_loc
-type token = M.token
-type lexer = M.lexer
+ELSE (* official camlp4 of ocaml >= 3.10 *)
+
+TODO
+
+END
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index e11cdd96f..087bfc5b7 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -32,14 +32,9 @@ module L =
 
 module G = Grammar.GMake(L)
 
-ELSE
+ELSE (* official camlp4 of ocaml >= 3.10 *)
 
-module L =
-  struct
-    let lexer = Lexer.lexer
-  end
-
-module G = Grammar.Make(L)
+TODO
 
 END
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 89a1c2ed5..914b6b8f6 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -19,19 +19,8 @@ let purge_str s =
   if String.length s == 0 || s.[0] <> '$' then s
   else String.sub s 1 (String.length s - 1)
 
-IFDEF OCAML308 THEN DEFINE NOP END
-IFDEF OCAML309 THEN DEFINE NOP END
-IFDEF CAMLP5 THEN DEFINE NOP END
-
 let anti loc x =
-  let e =
-    let loc =
-      IFDEF NOP THEN
-        loc
-      ELSE
-	(1, snd loc - fst loc)
-      END
-    in <:expr< $lid:purge_str x$ >>
+  let e = <:expr< $lid:purge_str x$ >>
   in
   <:expr< $anti:e$ >>
 
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 20cb01b16..0c15950ed 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -34,16 +34,10 @@ let rec iter_name i j base sep =
   if i >= j then base^(string_of_int i)
   else (iter_name i (j-1) base sep)^sep^" "^base^(string_of_int j)
 
-(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to
-   /dev/null, but for being compatible with earlier ocaml and not
-   relying on system-dependent stuff like open_out "/dev/null",
-   let's use instead a magical hack *)
-
 (* Standard printer, with a final newline *)
 let pr s = Printf.printf (s^^"\n")
 (* Printing to /dev/null *)
-let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ())
-	  : ('a, out_channel, unit) format -> 'a)
+let pn s = Printf.ifprintf stdout s
 (* Proof printer : prints iff gen_proof is true *)
 let pp = if gen_proof then pr else pn
 (* Printer for admitted parts : prints iff gen_proof is false *)