From 4422e16f529359bb96c7eee214b2b6648958ef48 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Tue, 18 Sep 2012 14:26:42 +0000 Subject: Cleaning interface of Util. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/command.ml | 2 +- toplevel/coqtop.ml | 2 +- toplevel/lemmas.ml | 2 +- toplevel/metasyntax.ml | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) (limited to 'toplevel') 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 -- cgit v1.2.3