Ensure that a function declared with a label is used with it

 This correspond to ocaml4 warning 6

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16053 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 18 insertions, 13 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 3b5034e95..1f4082b84 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -32,13 +32,16 @@ let load_rcfile() =
         if CUnix.file_readable_p !rcfile then
           Vernac.load_vernac false !rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
-      else try let inferedrc = List.find CUnix.file_readable_p [
-	Envars.xdg_config_home (fun x -> msg_warning (str x))/rcdefaultname^"."^Coq_config.version;
-	Envars.xdg_config_home (fun x -> msg_warning (str x))/rcdefaultname;
-	Envars.home (fun x -> msg_warning (str x))/"."^rcdefaultname^"."^Coq_config.version;
-	Envars.home (fun x -> msg_warning (str x))/"."^rcdefaultname;
-      ] in
-        Vernac.load_vernac false inferedrc
+      else
+	try
+	  let warn x = msg_warning (str x) in
+	  let inferedrc = List.find CUnix.file_readable_p [
+	    Envars.xdg_config_home warn / rcdefaultname^"."^Coq_config.version;
+	    Envars.xdg_config_home warn / rcdefaultname;
+	    Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
+	    Envars.home ~warn / "."^rcdefaultname
+	  ] in
+          Vernac.load_vernac false inferedrc
 	with Not_found -> ()
 	(*
 	Flags.if_verbose
@@ -91,9 +94,9 @@ let theories_dirs_map = [
 
 (* Initializes the LoadPath *)
 let init_load_path () =
-  let coqlib = Envars.coqlib Errors.error in
+  let coqlib = Envars.coqlib ~fail:Errors.error in
   let user_contrib = coqlib/"user-contrib" in
-  let xdg_dirs = Envars.xdg_dirs (fun x -> msg_warning (str x)) in
+  let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> msg_warning (str x)) in
   let coqpath = Envars.coqpath in
   let dirs = ["plugins"] in
     (* NOTE: These directories are searched from last to first *)
@@ -129,7 +132,7 @@ let init_ocaml_path () =
   let add_subdir dl =
     Mltop.add_ml_dir (List.fold_left (/) Envars.coqroot dl)
   in
-    Mltop.add_ml_dir (Envars.coqlib Errors.error);
+    Mltop.add_ml_dir (Envars.coqlib ~fail:Errors.error);
     List.iter add_subdir
       [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
 	[ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index ecd9cafac..b104ef4c8 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -23,7 +23,7 @@ let fatal_error info =
 
 let get_version_date () =
   try
-    let coqlib = Envars.coqlib Errors.error in
+    let coqlib = Envars.coqlib ~fail:Errors.error in
     let ch = open_in (Filename.concat coqlib "revision") in
     let ver = input_line ch in
     let rev = input_line ch in
@@ -295,7 +295,9 @@ let parse_args arglist =
     | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
     | "-coqlib" :: [] -> usage ()
 
-    | "-where" :: _ -> print_endline (Envars.coqlib Errors.error); exit (if !filter_opts then 2 else 0)
+    | "-where" :: _ ->
+        print_endline (Envars.coqlib ~fail:Errors.error);
+        exit (if !filter_opts then 2 else 0)
 
     | ("-config"|"--config") :: _ -> Usage.print_config (); exit (if !filter_opts then 2 else 0)
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 8e1864461..1bfc8f701 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -94,7 +94,7 @@ let print_usage_coqc () =
 
 let print_config () =
   if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n";
-  Printf.printf "COQLIB=%s/\n" (Envars.coqlib Errors.error);
+  Printf.printf "COQLIB=%s/\n" (Envars.coqlib ~fail:Errors.error);
   Printf.printf "DOCDIR=%s/\n" (Envars.docdir ());
   Printf.printf "OCAMLDEP=%s\n" Coq_config.ocamldep;
   Printf.printf "OCAMLC=%s\n" Coq_config.ocamlc;