Cleaning interface of Util.

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

23 files changed, 188 insertions, 262 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 5b58dc9ba..343c72788 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -370,4 +370,4 @@ open Printf
 
 let mem s =
   let m = try_find_library s in
-  h 0 (str (sprintf "%dk" (size_kb m)))
+  h 0 (str (sprintf "%dk" (CObj.size_kb m)))
diff --git a/checker/check.mllib b/checker/check.mllib
index d286651a1..2a6486ddd 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -7,6 +7,7 @@ Loc
 Segmenttree
 Unicodetable
 Errors
+CObj
 CList
 CArray
 Util
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 766c7c9be..0e7aec1a8 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -20,7 +20,7 @@ let memory_stat = ref false
 
 let print_memory_stat () =
   if !memory_stat then begin
-    Format.printf "total heap size = %d kbytes\n" (heap_size_kb ());
+    Format.printf "total heap size = %d kbytes\n" (CObj.heap_size_kb ());
     Format.print_newline();
     flush_all()
   end
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 562c58fed..286c6faea 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -8,6 +8,7 @@ Loc
 Segmenttree
 Unicodetable
 Errors
+CObj
 CList
 CArray
 Util
diff --git a/lib/cList.ml b/lib/cList.ml
index 3e4c0a4b3..3a4a2f566 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -66,6 +66,7 @@ sig
 
   (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *)
   val tabulate : (int -> 'a) -> int -> 'a list
+  val interval : int -> int -> int list
   val make : int -> 'a -> 'a list
   val assign : 'a list -> int -> 'a -> 'a list
   val distinct : 'a list -> bool
@@ -369,6 +370,12 @@ let tabulate f len =
   loop dummy 0;
   dummy.tail
 
+let interval n m =
+  let rec interval_n (l,m) =
+    if n > m then l else interval_n (m::l, pred m)
+  in
+  interval_n ([], m)
+
 let addn n v =
   let rec aux n l =
     if n = 0 then l
diff --git a/lib/cList.mli b/lib/cList.mli
index ef4406150..20b63dcd6 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -79,6 +79,10 @@ sig
   val tabulate : (int -> 'a) -> int -> 'a list
   (** [tabulate f n] builds [[f 0; ...; f (n-1)]] *)
 
+  val interval : int -> int -> int list
+  (** [interval i j] creates the list [[i; i + 1; ...; j]], or [[]] when 
+      [j <= i]. *)
+
   val make : int -> 'a -> 'a list
   (** [make n x] returns a list made of [n] times [x]. Raise
       [Invalid_argument "List.make"] if [n] is negative. *)
diff --git a/lib/cObj.ml b/lib/cObj.ml
new file mode 100644
index 000000000..ed14563df
--- /dev/null
+++ b/lib/cObj.ml
@@ -0,0 +1,111 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*s Logical and physical size of ocaml values. *)
+
+(** {6 Logical sizes} *)
+
+let c = ref 0
+let s = ref 0
+let b = ref 0
+let m = ref 0
+
+let rec obj_stats d t =
+  if Obj.is_int t then m := max d !m
+  else if Obj.tag t >= Obj.no_scan_tag then
+    if Obj.tag t = Obj.string_tag then
+      (c := !c + Obj.size t; b := !b + 1; m := max d !m)
+    else if Obj.tag t = Obj.double_tag then
+      (s := !s + 2; b := !b + 1; m := max d !m)
+    else if Obj.tag t = Obj.double_array_tag then
+      (s := !s + 2 * Obj.size t; b := !b + 1; m := max d !m)
+    else (b := !b + 1; m := max d !m)
+  else
+    let n = Obj.size t in
+    s := !s + n; b := !b + 1;
+    block_stats (d + 1) (n - 1) t
+
+and block_stats d i t =
+  if i >= 0 then (obj_stats d (Obj.field t i); block_stats d (i-1) t)
+
+let obj_stats a =
+  c := 0; s:= 0; b:= 0; m:= 0;
+  obj_stats 0 (Obj.repr a);
+  (!c, !s + !b, !m)
+
+(** {6 Physical sizes} *)
+
+(*s Pointers already visited are stored in a hash-table, where
+    comparisons are done using physical equality. *)
+
+module H = Hashtbl.Make(
+  struct
+    type t = Obj.t
+    let equal = (==)
+    let hash o = Hashtbl.hash (Obj.magic o : int)
+  end)
+
+let node_table = (H.create 257 : unit H.t)
+
+let in_table o = try H.find node_table o; true with Not_found -> false
+
+let add_in_table o = H.add node_table o ()
+
+let reset_table () = H.clear node_table
+
+(*s Objects are traversed recursively, as soon as their tags are less than
+    [no_scan_tag]. [count] records the numbers of words already visited. *)
+
+let size_of_double = Obj.size (Obj.repr 1.0)
+
+let count = ref 0
+
+let rec traverse t =
+  if not (in_table t) then begin
+    if Obj.is_block t then begin
+      add_in_table t;
+      let n = Obj.size t in
+      let tag = Obj.tag t in
+      if tag < Obj.no_scan_tag then begin
+        count := !count + 1 + n;
+        for i = 0 to n - 1 do
+          let f = Obj.field t i in traverse f
+        done
+      end else if tag = Obj.string_tag then
+        count := !count + 1 + n
+      else if tag = Obj.double_tag then
+        count := !count + size_of_double
+      else if tag = Obj.double_array_tag then
+        count := !count + 1 + size_of_double * n
+      else
+        incr count
+    end
+  end
+
+(*s Sizes of objects in words and in bytes. The size in bytes is computed
+    system-independently according to [Sys.word_size]. *)
+
+let size o =
+  reset_table ();
+  count := 0;
+  traverse (Obj.repr o);
+  !count
+
+let size_b o = (size o) * (Sys.word_size / 8)
+
+let size_kb o = (size o) / (8192 / Sys.word_size)
+
+(*s Total size of the allocated ocaml heap. *)
+
+let heap_size () =
+  let stat = Gc.stat ()
+  and control = Gc.get () in
+  let max_words_total = stat.Gc.heap_words + control.Gc.minor_heap_size in
+  (max_words_total * (Sys.word_size / 8))
+
+let heap_size_kb () = (heap_size () + 1023) / 1024
diff --git a/lib/cObj.mli b/lib/cObj.mli
new file mode 100644
index 000000000..61c778f1f
--- /dev/null
+++ b/lib/cObj.mli
@@ -0,0 +1,34 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** {6 Physical size of an ocaml value.}
+
+  These functions explore objects recursively and may allocate a lot. *)
+
+val size : 'a -> int
+(** Physical size of an object in words. *)
+
+val size_b : 'a -> int
+(** Same as [size] in bytes. *)
+
+val size_kb : 'a -> int
+(** Same as [size] in kilobytes. *)
+
+(** {6 Logical size of an OCaml value *)
+
+val obj_stats : 'a -> int * int * int
+(** Return the (logical) value size, the string size, and the maximum depth of
+    the object. This loops on cyclic structures. *)
+
+(** {6 Total size of the allocated ocaml heap. } *)
+
+val heap_size : unit -> int
+(** Heap size, in words. *)
+
+val heap_size_kb : unit -> int
+(** Heap size, in kilobytes. *)
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 3716a1021..0dd24d74c 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -4,6 +4,7 @@ Coq_config
 Segmenttree
 Unicodetable
 Deque
+CObj
 CList
 CArray
 Util
diff --git a/lib/profile.ml b/lib/profile.ml
index 9002972d9..b49a66e2f 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -657,80 +657,15 @@ let profile7 e f a b c d g h i =
     last_alloc := get_alloc ();
     raise exn
 
-(* Some utilities to compute the logical and physical sizes and depth
-   of ML objects *)
-
-let c = ref 0
-let s = ref 0
-let b = ref 0
-let m = ref 0
-
-let rec obj_stats d t =
-  if Obj.is_int t then m := max d !m
-  else if Obj.tag t >= Obj.no_scan_tag then
-    if Obj.tag t = Obj.string_tag then
-      (c := !c + Obj.size t; b := !b + 1; m := max d !m)
-    else if Obj.tag t = Obj.double_tag then
-      (s := !s + 2; b := !b + 1; m := max d !m)
-    else if Obj.tag t = Obj.double_array_tag then
-      (s := !s + 2 * Obj.size t; b := !b + 1; m := max d !m)
-    else (b := !b + 1; m := max d !m)
-  else
-    let n = Obj.size t in
-    s := !s + n; b := !b + 1;
-    block_stats (d + 1) (n - 1) t
-
-and block_stats d i t =
-  if i >= 0 then (obj_stats d (Obj.field t i); block_stats d (i-1) t)
-
-let obj_stats a =
-  c := 0; s:= 0; b:= 0; m:= 0;
-  obj_stats 0 (Obj.repr a);
-  (!c, !s + !b, !m)
-
-module H = Hashtbl.Make(
-  struct
-    type t = Obj.t
-    let equal = (==)
-    let hash o = Hashtbl.hash (Obj.magic o : int)
-  end)
-
-let tbl = H.create 13
-
-let rec obj_shared_size s t =
-  if Obj.is_int t then s
-  else if H.mem tbl t then s
-  else begin
-    H.add tbl t ();
-    let n = Obj.size t in
-    if Obj.tag t >= Obj.no_scan_tag then
-      if Obj.tag t = Obj.string_tag then (c := !c + n; s + 1)
-      else if Obj.tag t = Obj.double_tag then s + 3
-      else if Obj.tag t = Obj.double_array_tag then s + 2 * n + 1
-      else s + 1
-    else
-      block_shared_size (s + n + 1) (n - 1) t
-  end
-
-and block_shared_size s i t =
-  if i < 0 then s
-  else block_shared_size (obj_shared_size s (Obj.field t i)) (i-1) t
-
-let obj_shared_size a =
-  H.clear tbl;
-  c := 0;
-  let s = obj_shared_size 0 (Obj.repr a) in
-  (!c, s)
-
 let print_logical_stats a =
-  let (c, s, d) = obj_stats a in
+  let (c, s, d) = CObj.obj_stats a in
   Printf.printf "Expanded size: %10d (str: %8d) Depth: %6d\n" (s+c) c d
 
 let print_stats a =
-  let (c1, s, d) = obj_stats a in
-  let (c2, o) = obj_shared_size a in
-  Printf.printf "Size: %8d (str: %8d) (exp: %10d)  Depth: %6d\n"
-    (o + c2) c2 (s + c1) d
+  let (c1, s, d) = CObj.obj_stats a in
+  let c2 = CObj.size a in
+  Printf.printf "Size: %8d (exp: %10d)  Depth: %6d\n"
+    c2 (s + c1) d
 (*
 let _ = Gc.set { (Gc.get()) with Gc.verbose = 13 }
 *)
diff --git a/lib/profile.mli b/lib/profile.mli
index a67622fd2..812fd8b1e 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -113,12 +113,3 @@ val print_logical_stats : 'a -> unit
    This function allocates itself a lot (the same order of magnitude
    as the physical size of its argument) *)
 val print_stats : 'a -> unit
-
-(** Return logical size (first for strings, then for not strings),
-   (in words) and depth of its argument 
-   This function allocates itself a lot *)
-val obj_stats : 'a -> int * int * int
-
-(** Return physical size of its argument (string part and rest) 
-   This function allocates itself a lot *)
-val obj_shared_size : 'a -> int * int
diff --git a/lib/util.ml b/lib/util.ml
index 6f9f9bd83..6c1fc39b5 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -428,133 +428,6 @@ module Intset = Set.Make(struct type t = int let compare (x:t) (y:t) = compare x
 
 module Intmap = Map.Make(struct type t = int let compare (x:t) (y:t) = compare x y end)
 
-let intmap_in_dom x m =
-  try let _ = Intmap.find x m in true with Not_found -> false
-
-let intmap_to_list m = Intmap.fold (fun n v l -> (n,v)::l) m []
-
-let intmap_inv m b = Intmap.fold (fun n v l -> if v = b then n::l else l) m []
-
-let interval n m =
-  let rec interval_n (l,m) =
-    if n > m then l else interval_n (m::l,pred m)
-  in
-  interval_n ([],m)
-
-(*s Memoization *)
-
-let memo1_eq eq f =
-  let m = ref None in
-  fun x ->
-    match !m with
-        Some(x',y') when eq x x' -> y'
-      | _ -> let y = f x in m := Some(x,y); y
-
-let memo1_1 f = memo1_eq (==) f
-let memo1_2 f =
-  let f' =
-    memo1_eq (fun (x,y) (x',y') -> x==x' && y==y') (fun (x,y) -> f x y) in
-  (fun x y -> f'(x,y))
-
-(* Memorizes the last n distinct calls to f. Since there is no hash,
-   Efficient only for small n. *)
-let memon_eq eq n f =
-  let cache = ref [] in (* the cache: a stack *)
-  let m = ref 0 in      (* usage of the cache *)
-  let rec find x = function
-    | (x',y')::l when eq x x' -> y', l (* cell is moved to the top *)
-    | [] -> (* we assume n>0, so creating one memo cell is OK *)
-        incr m; (f x, [])
-    | [_] when !m>=n -> f x,[] (* cache is full: dispose of last cell *)
-    | p::l (* not(eq x (fst p)) *) -> let (y,l') = find x l in (y, p::l')
-  in
-  (fun x ->
-    let (y,l) = find x !cache in
-    cache := (x,y)::l;
-    y)
-
-
-(*s Size of ocaml values. *)
-
-module Size = struct
-
-  (*s Pointers already visited are stored in a hash-table, where
-      comparisons are done using physical equality. *)
-
-  module H = Hashtbl.Make(
-    struct
-      type t = Obj.t
-      let equal = (==)
-      let hash o = Hashtbl.hash (Obj.magic o : int)
-    end)
-
-  let node_table = (H.create 257 : unit H.t)
-
-  let in_table o = try H.find node_table o; true with Not_found -> false
-
-  let add_in_table o = H.add node_table o ()
-
-  let reset_table () = H.clear node_table
-
-  (*s Objects are traversed recursively, as soon as their tags are less than
-      [no_scan_tag]. [count] records the numbers of words already visited. *)
-
-  let size_of_double = Obj.size (Obj.repr 1.0)
-
-  let count = ref 0
-
-  let rec traverse t =
-    if not (in_table t) then begin
-      add_in_table t;
-      if Obj.is_block t then begin
-	let n = Obj.size t in
-	let tag = Obj.tag t in
-	if tag < Obj.no_scan_tag then begin
-	  count := !count + 1 + n;
-	  for i = 0 to n - 1 do
-      	    let f = Obj.field t i in
-	    if Obj.is_block f then traverse f
-	  done
-	end else if tag = Obj.string_tag then
-	  count := !count + 1 + n
-	else if tag = Obj.double_tag then
-	  count := !count + size_of_double
-	else if tag = Obj.double_array_tag then
-	  count := !count + 1 + size_of_double * n
-	else
-	  incr count
-      end
-    end
-
-  (*s Sizes of objects in words and in bytes. The size in bytes is computed
-      system-independently according to [Sys.word_size]. *)
-
-  let size_w o =
-    reset_table ();
-    count := 0;
-    traverse (Obj.repr o);
-    !count
-
-  let size_b o = (size_w o) * (Sys.word_size / 8)
-
-  let size_kb o = (size_w o) / (8192 / Sys.word_size)
-
-end
-
-let size_w = Size.size_w
-let size_b = Size.size_b
-let size_kb = Size.size_kb
-
-(*s Total size of the allocated ocaml heap. *)
-
-let heap_size () =
-  let stat = Gc.stat ()
-  and control = Gc.get () in
-  let max_words_total = stat.Gc.heap_words + control.Gc.minor_heap_size in
-  (max_words_total * (Sys.word_size / 8))
-
-let heap_size_kb () = (heap_size () + 1023) / 1024
-
 (*s interruption *)
 
 let interrupt = ref false
diff --git a/lib/util.mli b/lib/util.mli
index a7586547e..1333d1854 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -15,11 +15,6 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
 val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b
 val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b
 
-(** Going down pairs *)
-
-val down_fst : ('a -> 'b) -> 'a * 'c -> 'b
-val down_snd : ('a -> 'b) -> 'c * 'a -> 'b
-
 (** Mapping under triple *)
 
 val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd
@@ -106,46 +101,12 @@ val delayed_force : 'a delayed -> 'a
 
 (** {6 Misc. } *)
 
-type ('a,'b) union = Inl of 'a | Inr of 'b
+type ('a, 'b) union = Inl of 'a | Inr of 'b
 
 module Intset : Set.S with type elt = int
 
 module Intmap : Map.S with type key = int
 
-val intmap_in_dom : int -> 'a Intmap.t -> bool
-val intmap_to_list : 'a Intmap.t -> (int * 'a) list
-val intmap_inv : 'a Intmap.t -> 'a -> int list
-
-val interval : int -> int -> int list
-
-(** {6 Memoization. } *)
-
-(** General comments on memoization:
-   - cache is created whenever the function is supplied (because of
-      ML's polymorphic value restriction).
-   - cache is never flushed (unless the memoized fun is GC'd)
- 
-   One cell memory: memorizes only the last call *)
-val memo1_1 : ('a -> 'b) -> ('a -> 'b)
-val memo1_2 : ('a -> 'b -> 'c) -> ('a -> 'b -> 'c)
-
-(** with custom equality (used to deal with various arities) *)
-val memo1_eq : ('a -> 'a -> bool) -> ('a -> 'b) -> ('a -> 'b)
-
-(** Memorizes the last [n] distinct calls. Efficient only for small [n]. *)
-val memon_eq : ('a -> 'a -> bool) -> int -> ('a -> 'b) -> ('a -> 'b)
-
-(** {6 Size of an ocaml value (in words, bytes and kilobytes). } *)
-
-val size_w : 'a -> int
-val size_b : 'a -> int
-val size_kb : 'a -> int
-
-(** {6 Total size of the allocated ocaml heap. } *)
-
-val heap_size : unit -> int
-val heap_size_kb : unit -> int
-
 (** {6 ... } *)
 (** Coq interruption: set the following boolean reference to interrupt Coq
     (it eventually raises [Break], simulating a Ctrl-C) *)
diff --git a/library/library.ml b/library/library.ml
index bca44726d..9c881e515 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -665,5 +665,5 @@ open Printf
 let mem s =
   let m = try_find_library s in
   h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
-		 (size_kb m) (size_kb m.library_compiled)
-		 (size_kb m.library_objects)))
+		 (CObj.size_kb m) (CObj.size_kb m.library_compiled)
+		 (CObj.size_kb m.library_objects)))
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ef0de36f5..843b4b9a4 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -333,7 +333,7 @@ and extract_type_scheme env db c p =
       | _ ->
           let rels = fst (splay_prod env none (type_of env c)) in
           let env = push_rels_assum rels env in
-          let eta_args = List.rev_map mkRel (interval 1 p) in
+          let eta_args = List.rev_map mkRel (List.interval 1 p) in
           extract_type env db 0 (lift p c) eta_args
 
 
@@ -719,7 +719,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let oi = mi.ind_packets.(i) in
   let nb_tvars = List.length oi.ip_vars
   and types = List.map (expand env) oi.ip_types.(j-1) in
-  let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in
+  let list_tvar = List.map (fun i -> Tvar i) (List.interval 1 nb_tvars) in
   let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
   let type_cons = instantiation (nb_tvars, type_cons) in
   (* Then, the usual variables [s], [ls], [la], ... *)
@@ -848,7 +848,7 @@ let decomp_lams_eta_n n m env c t =
   let d = n - m in
   (* we'd better keep rels' as long as possible. *)
   let rels = (List.firstn d rels) @ rels' in
-  let eta_args = List.rev_map mkRel (interval 1 d) in
+  let eta_args = List.rev_map mkRel (List.interval 1 d) in
   rels, applist (lift d c,eta_args)
 
 (* Let's try to identify some situation where extracted code
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index af3227729..e51415abb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -100,9 +100,16 @@ let is_ground_env evd env =
     | _ -> true in
   List.for_all is_ground_decl (rel_context env) &&
   List.for_all is_ground_decl (named_context env)
+
 (* Memoization is safe since evar_map and environ are applicative
    structures *)
-let is_ground_env = memo1_2 is_ground_env
+let memo f =
+  let m = ref None in
+  fun x y -> match !m with
+  | Some (x', y', r) when x == x' && y == y' -> r
+  | _ -> let r = f x y in m := Some (x, y, r); r
+
+let is_ground_env = memo is_ground_env
 
 (* Return the head evar if any *)
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 4062117b0..de6873ba3 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -82,7 +82,7 @@ let mis_is_recursive_subset listind rarg =
   Array.exists one_is_rec (dest_subterms rarg)
 
 let mis_is_recursive (ind,mib,mip) =
-  mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1))
+  mis_is_recursive_subset (List.interval 0 (mib.mind_ntypes - 1))
     mip.mind_recargs
 
 let mis_nf_constructor_type (ind,mib,mip) j =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a35cf537e..08b05746b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -656,7 +656,7 @@ let descend_then sigma env head dirn =
 	it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in
       let brl =
         List.map build_branch
-          (interval 1 (Array.length mip.mind_consnames)) in
+          (List.interval 1 (Array.length mip.mind_consnames)) in
       let ci = make_case_info env ind RegularStyle in
       mkCase (ci, p, head, Array.of_list brl)))
 
@@ -699,7 +699,7 @@ let construct_discriminator sigma env dirn c sort =
     let endpt = if i = dirn then true_0 else false_0 in
     it_mkLambda_or_LetIn endpt cstrs.(i-1).cs_args in
   let brl =
-    List.map build_branch(interval 1 (Array.length mip.mind_consnames)) in
+    List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
   let ci = make_case_info env ind RegularStyle in
   mkCase (ci, p, c, Array.of_list brl)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 69b446f90..bdf2ea96d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1247,7 +1247,7 @@ let any_constructor with_evars tacopt gl =
   tclFIRST
     (List.map
       (fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t)
-      (interval 1 nconstr)) gl
+      (List.interval 1 nconstr)) gl
 
 let left_with_bindings  with_evars = constructor_tac with_evars (Some 2) 1
 let right_with_bindings with_evars = constructor_tac with_evars (Some 2) 2
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 044502cda..873cfb09e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -534,7 +534,7 @@ let compute_possible_guardness_evidences (ids,_,na) =
 	 but doing it properly involves delta-reduction, and it finally
          doesn't seem to worth the effort (except for huge mutual
 	 fixpoints ?) *)
-      interval 0 (List.length ids - 1)
+      List.interval 0 (List.length ids - 1)
 
 type recursive_preentry =
   identifier list * constr option list * types list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index df155eebb..fe612f710 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -41,7 +41,7 @@ let memory_stat = ref false
 
 let print_memory_stat () =
   if !memory_stat then
-    pp (str "total heap size = " ++ int (heap_size_kb ()) ++ str " kbytes" ++ fnl ())
+    pp (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes" ++ fnl ())
 
 let _ = at_exit print_memory_stat
 
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 25a8e9208..1c8302c1a 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -51,7 +51,7 @@ let adjust_guardness_conditions const = function
   | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
 (*      let possible_indexes =
 	List.map2 (fun i c -> match i with Some i -> i | None ->
-	  interval 0 (List.length ((lam_assum c))))
+	  List.interval 0 (List.length ((lam_assum c))))
 	  lemma_guard (Array.to_list fixdefs) in
 *)
       let indexes =
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 534a0a7dd..a665dc373 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -831,7 +831,7 @@ let internalization_type_of_entry_type = function
   | ETBinderList _ | ETConstrList _ -> assert false
 
 let set_internalization_type typs =
-  List.map (down_snd internalization_type_of_entry_type) typs
+  List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
 
 let make_internalization_vars recvars mainvars typs =
   let maintyps = List.combine mainvars typs in