aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--INSTALL4
-rw-r--r--INSTALL.ide2
-rw-r--r--Makefile.build8
-rw-r--r--configure.ml4
-rw-r--r--dev/doc/debugging.txt8
-rw-r--r--dev/doc/patch.ocaml-3.10.drop.rectypes31
-rw-r--r--dev/include3
-rw-r--r--lib/cArray.ml30
-rw-r--r--lib/cArray.mli32
-rw-r--r--lib/cList.ml45
-rw-r--r--lib/cList.mli47
-rw-r--r--lib/cString.ml36
-rw-r--r--lib/cString.mli37
-rw-r--r--tools/coqdoc/cpretty.mll9
14 files changed, 18 insertions, 278 deletions
diff --git a/INSTALL b/INSTALL
index ca8d705c5..276c57601 100644
--- a/INSTALL
+++ b/INSTALL
@@ -41,7 +41,7 @@ WHAT DO YOU NEED ?
Should you need or prefer to compile Coq V8.4 yourself, you need:
- - Objective Caml version 3.11.2 or later
+ - Objective Caml version 3.12.1 or later
(available at http://caml.inria.fr/)
- Camlp5 (version <= 4.08, or 5.* transitional)
@@ -88,7 +88,7 @@ QUICK INSTALLATION PROCEDURE.
INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
=================================================
-1- Check that you have the Objective Caml compiler version 3.11.2 (or later)
+1- Check that you have the Objective Caml compiler version 3.12.1 (or later)
installed on your computer and that "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 b06fab1f6..2bbb4a5fc 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.11.2 with native threads support.
+ - OCaml >= 3.12.1 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.24.x.
diff --git a/Makefile.build b/Makefile.build
index f8895b2ed..7bfc6f953 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -106,7 +106,7 @@ OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS)
BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
-DEPFLAGS= $(LOCALINCLUDES)
+DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils
define bestocaml
$(if $(OPT),\
@@ -928,10 +928,10 @@ endif
$(SHOW)'CAMLP4DEPS $<'
$(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(call CAMLP4DEPS,$<)" $(TOTARGET)
-# We now use coqdep_boot to wrap around ocamldep -modules, since it is aware
-# of .ml4 files
+# Since OCaml 3.12.1, we could use again ocamldep directly, thanks to
+# the option -ml-synonym
-OCAMLDEP_NG = $(COQDEPBOOT) -mldep $(OCAMLDEP)
+OCAMLDEP_NG = $(OCAMLDEP) -slash -ml-synonym .ml4
checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
$(SHOW)'OCAMLDEP $<'
diff --git a/configure.ml b/configure.ml
index 1c037269d..569e6ebd4 100644
--- a/configure.ml
+++ b/configure.ml
@@ -493,14 +493,14 @@ let caml_version_nums =
"Is it installed properly?")
let check_caml_version () =
- if caml_version_nums >= [3;11;2] then
+ if caml_version_nums >= [3;12;1] then
printf "You have OCaml %s. Good!\n" caml_version
else
let () = printf "Your version of OCaml is %s.\n" caml_version in
if !Prefs.force_caml_version then
printf "*Warning* Your version of OCaml is outdated.\n"
else
- die "You need OCaml 3.11.2 or later."
+ die "You need OCaml 3.12.1 or later."
let _ = check_caml_version ()
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 2480b8edb..f0df2fc37 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -21,14 +21,6 @@ Debugging from Coq toplevel using Caml trace mechanism
notations, ...), use "Set Printing All". It will affect the #trace
printers too.
-Note for Ocaml 3.10.x: Ocaml 3.10.x requires that modules compiled
-with -rectypes are loaded in an environment with -rectypes set but
-there is no way to tell the toplevel to support -rectypes. To make it
-works, use "patch -p0 < dev/doc/patch.ocaml-3.10.drop.rectypes" to
-hack script/coqmktop.ml, then recompile coqtop.byte. The procedure
-above then works as soon as coqtop.byte is called with at least one
-argument (add neutral option -byte to ensure at least one argument).
-
Debugging from Caml debugger
============================
diff --git a/dev/doc/patch.ocaml-3.10.drop.rectypes b/dev/doc/patch.ocaml-3.10.drop.rectypes
deleted file mode 100644
index ba7a3e950..000000000
--- a/dev/doc/patch.ocaml-3.10.drop.rectypes
+++ /dev/null
@@ -1,31 +0,0 @@
-Index: scripts/coqmktop.ml
-===================================================================
---- scripts/coqmktop.ml (révision 12084)
-+++ scripts/coqmktop.ml (copie de travail)
-@@ -231,12 +231,25 @@
- end;;
-
- let ppf = Format.std_formatter;;
-+ let set_rectypes_hack () =
-+ if String.length (Sys.ocaml_version) >= 4 &
-+ String.sub (Sys.ocaml_version) 0 4 = \"3.10\"
-+ then
-+ (* ocaml 3.10 does not have #rectypes but needs it *)
-+ (* simulate a call with option -rectypes before *)
-+ (* jumping to the ocaml toplevel *)
-+ for i = 1 to Array.length Sys.argv - 1 do
-+ Sys.argv.(i) <- \"-rectypes\"
-+ done
-+ else
-+ () in
-+
- Mltop.set_top
- {Mltop.load_obj=
- (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\");
- Mltop.use_file=Topdirs.dir_use ppf;
- Mltop.add_dir=Topdirs.dir_directory;
-- Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"
-+ Mltop.ml_loop=(fun () -> set_rectypes_hack(); Topmain.main()) };;\n"
-
- (* create a temporary main file to link *)
- let create_tmp_main_file modules =
diff --git a/dev/include b/dev/include
index 9518034df..5eea5cc03 100644
--- a/dev/include
+++ b/dev/include
@@ -10,8 +10,9 @@
Alternatively, you can avoid typing #use "include" after each Drop
by adding the following lines in your $HOME/.ocamlinit :
+ #directory "+compiler-libs";;
if Filename.basename Sys.argv.(0) = "coqtop.byte"
- then ignore (Toploop.use_silently Format.std_formatter "include")
+ then ignore (Toploop.use_silently Format.std_formatter "dev/include")
*)
(* For OCaml 3.10.x:
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 77fb04322..ab3a4ba51 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -6,35 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-module type S =
-sig
- external length : 'a array -> int = "%array_length"
- external get : 'a array -> int -> 'a = "%array_safe_get"
- external set : 'a array -> int -> 'a -> unit = "%array_safe_set"
- external make : int -> 'a -> 'a array = "caml_make_vect"
- val init : int -> (int -> 'a) -> 'a array
- val make_matrix : int -> int -> 'a -> 'a array array
- val create_matrix : int -> int -> 'a -> 'a array array
- val append : 'a array -> 'a array -> 'a array
- val concat : 'a array list -> 'a array
- val sub : 'a array -> int -> int -> 'a array
- val copy : 'a array -> 'a array
- val fill : 'a array -> int -> int -> 'a -> unit
- val blit : 'a array -> int -> 'a array -> int -> int -> unit
- val to_list : 'a array -> 'a list
- val of_list : 'a list -> 'a array
- val iter : ('a -> unit) -> 'a array -> unit
- val map : ('a -> 'b) -> 'a array -> 'b array
- val iteri : (int -> 'a -> unit) -> 'a array -> unit
- val mapi : (int -> 'a -> 'b) -> 'a array -> 'b array
- val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
- val fold_right : ('b -> 'a -> 'a) -> 'b array -> 'a -> 'a
- val sort : ('a -> 'a -> int) -> 'a array -> unit
- val stable_sort : ('a -> 'a -> int) -> 'a array -> unit
- val fast_sort : ('a -> 'a -> int) -> 'a array -> unit
- external unsafe_get : 'a array -> int -> 'a = "%array_unsafe_get"
- external unsafe_set : 'a array -> int -> 'a -> unit = "%array_unsafe_set"
-end
+module type S = module type of Array
module type ExtS =
sig
diff --git a/lib/cArray.mli b/lib/cArray.mli
index 83036e27c..e3a3bd7f5 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -6,37 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
-
-module type S =
-sig
- external length : 'a array -> int = "%array_length"
- external get : 'a array -> int -> 'a = "%array_safe_get"
- external set : 'a array -> int -> 'a -> unit = "%array_safe_set"
- external make : int -> 'a -> 'a array = "caml_make_vect"
- val init : int -> (int -> 'a) -> 'a array
- val make_matrix : int -> int -> 'a -> 'a array array
- val create_matrix : int -> int -> 'a -> 'a array array
- val append : 'a array -> 'a array -> 'a array
- val concat : 'a array list -> 'a array
- val sub : 'a array -> int -> int -> 'a array
- val copy : 'a array -> 'a array
- val fill : 'a array -> int -> int -> 'a -> unit
- val blit : 'a array -> int -> 'a array -> int -> int -> unit
- val to_list : 'a array -> 'a list
- val of_list : 'a list -> 'a array
- val iter : ('a -> unit) -> 'a array -> unit
- val map : ('a -> 'b) -> 'a array -> 'b array
- val iteri : (int -> 'a -> unit) -> 'a array -> unit
- val mapi : (int -> 'a -> 'b) -> 'a array -> 'b array
- val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
- val fold_right : ('b -> 'a -> 'a) -> 'b array -> 'a -> 'a
- val sort : ('a -> 'a -> int) -> 'a array -> unit
- val stable_sort : ('a -> 'a -> int) -> 'a array -> unit
- val fast_sort : ('a -> 'a -> int) -> 'a array -> unit
- external unsafe_get : 'a array -> int -> 'a = "%array_unsafe_get"
- external unsafe_set : 'a array -> int -> 'a -> unit = "%array_unsafe_set"
-end
+module type S = module type of Array
module type ExtS =
sig
diff --git a/lib/cList.ml b/lib/cList.ml
index 1a1993cd6..385c80b62 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -9,50 +9,7 @@
type 'a cmp = 'a -> 'a -> int
type 'a eq = 'a -> 'a -> bool
-module type S =
-sig
- val length : 'a list -> int
- val hd : 'a list -> 'a
- val tl : 'a list -> 'a list
- val nth : 'a list -> int -> 'a
- val rev : 'a list -> 'a list
- val append : 'a list -> 'a list -> 'a list
- val rev_append : 'a list -> 'a list -> 'a list
- val concat : 'a list list -> 'a list
- val flatten : 'a list list -> 'a list
- val iter : ('a -> unit) -> 'a list -> unit
- val map : ('a -> 'b) -> 'a list -> 'b list
- val rev_map : ('a -> 'b) -> 'a list -> 'b list
- val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
- val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
- val iter2 : ('a -> 'b -> unit) -> 'a list -> 'b list -> unit
- val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
- val rev_map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
- val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
- val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
- val for_all : ('a -> bool) -> 'a list -> bool
- val exists : ('a -> bool) -> 'a list -> bool
- val for_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
- val exists2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
- val mem : 'a -> 'a list -> bool
- val memq : 'a -> 'a list -> bool
- val find : ('a -> bool) -> 'a list -> 'a
- val filter : ('a -> bool) -> 'a list -> 'a list
- val find_all : ('a -> bool) -> 'a list -> 'a list
- val partition : ('a -> bool) -> 'a list -> 'a list * 'a list
- val assoc : 'a -> ('a * 'b) list -> 'b
- val assq : 'a -> ('a * 'b) list -> 'b
- val mem_assoc : 'a -> ('a * 'b) list -> bool
- val mem_assq : 'a -> ('a * 'b) list -> bool
- val remove_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list
- val remove_assq : 'a -> ('a * 'b) list -> ('a * 'b) list
- val split : ('a * 'b) list -> 'a list * 'b list
- val combine : 'a list -> 'b list -> ('a * 'b) list
- val sort : ('a -> 'a -> int) -> 'a list -> 'a list
- val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list
- val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list
- val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
-end
+module type S = module type of List
module type ExtS =
sig
diff --git a/lib/cList.mli b/lib/cList.mli
index 6af32fdd0..15900260c 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -6,56 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
-
type 'a cmp = 'a -> 'a -> int
type 'a eq = 'a -> 'a -> bool
(** Module type [S] is the one from OCaml Stdlib. *)
-module type S =
-sig
- val length : 'a list -> int
- val hd : 'a list -> 'a
- val tl : 'a list -> 'a list
- val nth : 'a list -> int -> 'a
- val rev : 'a list -> 'a list
- val append : 'a list -> 'a list -> 'a list
- val rev_append : 'a list -> 'a list -> 'a list
- val concat : 'a list list -> 'a list
- val flatten : 'a list list -> 'a list
- val iter : ('a -> unit) -> 'a list -> unit
- val map : ('a -> 'b) -> 'a list -> 'b list
- val rev_map : ('a -> 'b) -> 'a list -> 'b list
- val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
- val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
- val iter2 : ('a -> 'b -> unit) -> 'a list -> 'b list -> unit
- val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
- val rev_map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
- val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
- val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
- val for_all : ('a -> bool) -> 'a list -> bool
- val exists : ('a -> bool) -> 'a list -> bool
- val for_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
- val exists2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
- val mem : 'a -> 'a list -> bool
- val memq : 'a -> 'a list -> bool
- val find : ('a -> bool) -> 'a list -> 'a
- val filter : ('a -> bool) -> 'a list -> 'a list
- val find_all : ('a -> bool) -> 'a list -> 'a list
- val partition : ('a -> bool) -> 'a list -> 'a list * 'a list
- val assoc : 'a -> ('a * 'b) list -> 'b
- val assq : 'a -> ('a * 'b) list -> 'b
- val mem_assoc : 'a -> ('a * 'b) list -> bool
- val mem_assq : 'a -> ('a * 'b) list -> bool
- val remove_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list
- val remove_assq : 'a -> ('a * 'b) list -> ('a * 'b) list
- val split : ('a * 'b) list -> 'a list * 'b list
- val combine : 'a list -> 'b list -> ('a * 'b) list
- val sort : ('a -> 'a -> int) -> 'a list -> 'a list
- val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list
- val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list
- val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
-end
+module type S = module type of List
module type ExtS =
sig
diff --git a/lib/cString.ml b/lib/cString.ml
index 9be81bd3d..5c857077a 100644
--- a/lib/cString.ml
+++ b/lib/cString.ml
@@ -6,41 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** FIXME: use module type of *)
-module type S =
-sig
- external length : string -> int = "%string_length"
- external get : string -> int -> char = "%string_safe_get"
- external set : string -> int -> char -> unit = "%string_safe_set"
- external create : int -> string = "caml_create_string"
- val make : int -> char -> string
- val copy : string -> string
- val sub : string -> int -> int -> string
- val fill : string -> int -> int -> char -> unit
- val blit : string -> int -> string -> int -> int -> unit
- val concat : string -> string list -> string
- val iter : (char -> unit) -> string -> unit
- val escaped : string -> string
- val index : string -> char -> int
- val rindex : string -> char -> int
- val index_from : string -> int -> char -> int
- val rindex_from : string -> int -> char -> int
- val contains : string -> char -> bool
- val contains_from : string -> int -> char -> bool
- val rcontains_from : string -> int -> char -> bool
- val uppercase : string -> string
- val lowercase : string -> string
- val capitalize : string -> string
- val uncapitalize : string -> string
- type t = string
- val compare: t -> t -> int
- external unsafe_get : string -> int -> char = "%string_unsafe_get"
- external unsafe_set : string -> int -> char -> unit = "%string_unsafe_set"
- external unsafe_blit :
- string -> int -> string -> int -> int -> unit = "caml_blit_string" "noalloc"
- external unsafe_fill :
- string -> int -> int -> char -> unit = "caml_fill_string" "noalloc"
-end
+module type S = module type of String
module type ExtS =
sig
diff --git a/lib/cString.mli b/lib/cString.mli
index 5f3616231..6aa10875c 100644
--- a/lib/cString.mli
+++ b/lib/cString.mli
@@ -6,43 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
-
(** Module type [S] is the one from OCaml Stdlib. *)
-module type S =
-sig
- external length : string -> int = "%string_length"
- external get : string -> int -> char = "%string_safe_get"
- external set : string -> int -> char -> unit = "%string_safe_set"
- external create : int -> string = "caml_create_string"
- val make : int -> char -> string
- val copy : string -> string
- val sub : string -> int -> int -> string
- val fill : string -> int -> int -> char -> unit
- val blit : string -> int -> string -> int -> int -> unit
- val concat : string -> string list -> string
- val iter : (char -> unit) -> string -> unit
- val escaped : string -> string
- val index : string -> char -> int
- val rindex : string -> char -> int
- val index_from : string -> int -> char -> int
- val rindex_from : string -> int -> char -> int
- val contains : string -> char -> bool
- val contains_from : string -> int -> char -> bool
- val rcontains_from : string -> int -> char -> bool
- val uppercase : string -> string
- val lowercase : string -> string
- val capitalize : string -> string
- val uncapitalize : string -> string
- type t = string
- val compare: t -> t -> int
- external unsafe_get : string -> int -> char = "%string_unsafe_get"
- external unsafe_set : string -> int -> char -> unit = "%string_unsafe_set"
- external unsafe_blit :
- string -> int -> string -> int -> int -> unit = "caml_blit_string" "noalloc"
- external unsafe_fill :
- string -> int -> int -> char -> unit = "caml_fill_string" "noalloc"
-end
+module type S = module type of String
module type ExtS =
sig
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 2c58a05e2..d8a30ee36 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -12,13 +12,6 @@
open Printf
open Lexing
- (* A function that emulates Lexing.new_line (which does not exist in OCaml < 3.11.0) *)
- let new_line lexbuf =
- let pos = lexbuf.lex_curr_p in
- lexbuf.lex_curr_p <- { pos with
- pos_lnum = pos.pos_lnum + 1;
- pos_bol = pos.pos_cnum }
-
(* A list function we need *)
let rec take n ls =
if n = 0 then [] else
@@ -1065,7 +1058,7 @@ and body_bol = parse
| _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
and body = parse
- | nl {Tokens.flush_sublexer(); Output.line_break(); new_line lexbuf; body_bol lexbuf}
+ | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf}
| nl+ space* "]]" space* nl
{ Tokens.flush_sublexer();
if not !formatted then
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 08:54:31 +0000