diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-18 14:26:42 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-18 14:26:42 +0000 |
| commit | 4422e16f529359bb96c7eee214b2b6648958ef48 (patch) | |
| tree | c8d77ca4070bcbc0ce2fc630564fedd9043fafed /toplevel | |
| parent | 7208928de37565a9e38f9540f2bfb1e7a3b877e6 (diff) | |
Cleaning interface of Util.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -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 |
4 files changed, 4 insertions, 4 deletions
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 |