diff options
-rw-r--r-- | checker/check.ml | 2 | ||||
-rw-r--r-- | checker/check.mllib | 1 | ||||
-rw-r--r-- | checker/check_stat.ml | 2 | ||||
-rw-r--r-- | dev/printers.mllib | 1 | ||||
-rw-r--r-- | lib/cList.ml | 7 | ||||
-rw-r--r-- | lib/cList.mli | 4 | ||||
-rw-r--r-- | lib/cObj.ml | 111 | ||||
-rw-r--r-- | lib/cObj.mli | 34 | ||||
-rw-r--r-- | lib/clib.mllib | 1 | ||||
-rw-r--r-- | lib/profile.ml | 75 | ||||
-rw-r--r-- | lib/profile.mli | 9 | ||||
-rw-r--r-- | lib/util.ml | 127 | ||||
-rw-r--r-- | lib/util.mli | 41 | ||||
-rw-r--r-- | library/library.ml | 4 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 6 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 9 | ||||
-rw-r--r-- | pretyping/inductiveops.ml | 2 | ||||
-rw-r--r-- | tactics/equality.ml | 4 | ||||
-rw-r--r-- | tactics/tactics.ml | 2 | ||||
-rw-r--r-- | toplevel/command.ml | 2 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
-rw-r--r-- | toplevel/lemmas.ml | 2 | ||||
-rw-r--r-- | toplevel/metasyntax.ml | 2 |
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 |