aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/checker.ml
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-09-28 15:32:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-09-28 15:32:14 +0000
commit5754edd0bfc8c38cee2e721ef8d2130c97664f05 (patch)
tree523fdec4b715c5e79fa8e679684dd41697e3d6c2 /checker/checker.ml
parent86919192359dee7e274ab4af17bd32efe11a5f44 (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.ml24
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 := []