aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorppedrot2012-09-14 16:17:09 +0000
committerppedrot2012-09-14 16:17:09 +0000
commitf8394a52346bf1e6f98e7161e75fb65bd0631391 (patch)
treeae133cc5207283e8c5a89bb860435b37cbf6ecdb /tools
parent6dae53d279afe2b8dcfc43dd2aded9431944c5c8 (diff)
Moving Utils.list_* to a proper CList module, which includes stdlib
List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 7e400a332f..b6268f2336 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -158,7 +158,7 @@ let vars_to_put_by_root var_x_files_l (inc_i,inc_r) =
if inc_r = [] then
[".","$(INSTALLDEFAULTROOT)",[]]
else
- Util.list_fold_left_i (fun i out (pdir,ldir,abspdir) ->
+ Util.List.fold_left_i (fun i out (pdir,ldir,abspdir) ->
let vars_r = var_filter (List.exists (is_prefix abspdir)) (fun x -> x^string_of_int i) in
let pdir' = physical_dir_of_logical_dir ldir in
(pdir,pdir',vars_r)::out) 1 [] inc_r