diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-28 15:32:14 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-28 15:32:14 +0000 |
commit | 5754edd0bfc8c38cee2e721ef8d2130c97664f05 (patch) | |
tree | 523fdec4b715c5e79fa8e679684dd41697e3d6c2 /checker/checker.ml | |
parent | 86919192359dee7e274ab4af17bd32efe11a5f44 (diff) |
Fix function applications without labels (OCaml warning 6)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13469 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/checker.ml')
-rw-r--r-- | checker/checker.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 9646141d0..e8cc52ecf 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -72,17 +72,17 @@ let convert_string d = flush_all (); failwith "caught" -let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath = - if exists_dir dir then - let dirs = all_subdirs dir in - let prefix = repr_dirpath coq_dirpath in +let add_rec_path ~unix_path ~coq_root = + if exists_dir unix_path then + let dirs = all_subdirs ~unix_path in + let prefix = repr_dirpath coq_root in let convert_dirs (lp,cp) = (lp,make_dirpath (List.map convert_string (List.rev cp)@prefix)) in let dirs = map_succeed convert_dirs dirs in List.iter Check.add_load_path dirs; - Check.add_load_path (dir,coq_dirpath) + Check.add_load_path (unix_path, coq_root) else - msg_warning (str ("Cannot open " ^ dir)) + msg_warning (str ("Cannot open " ^ unix_path)) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -105,21 +105,21 @@ let init_load_path () = let plugins = coqlib/"plugins" in (* first user-contrib *) if Sys.file_exists user_contrib then - add_rec_path user_contrib Check.default_root_prefix; + add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix; (* then plugins *) - add_rec_path plugins (Names.make_dirpath [coq_root]); + add_rec_path ~unix_path:plugins ~coq_root:(Names.make_dirpath [coq_root]); (* then standard library *) (* List.iter (fun (s,alias) -> add_rec_path (coqlib/s) ([alias; coq_root])) theories_dirs_map;*) - add_rec_path (coqlib/"theories") (Names.make_dirpath[coq_root]); + add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.make_dirpath[coq_root]); (* then current directory *) - add_path "." Check.default_root_prefix; + add_path ~unix_path:"." ~coq_root:Check.default_root_prefix; (* additional loadpath, given with -I -include -R options *) List.iter - (fun (s,alias,reci) -> - if reci then add_rec_path s alias else add_path s alias) + (fun (unix_path, coq_root, reci) -> + if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root) (List.rev !includes); includes := [] |