[checker] fixed vo validation problems, module incompatibilities remain

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

1 files changed, 6 insertions, 4 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 712566a00..e15c37e67 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -295,7 +295,7 @@ let rec explain_exn = function
       hov 0 (anomaly_string () ++ str "Uncaught exception " ++
 	       str (Printexc.to_string reraise)++report())
 
-let parse_args() =
+let parse_args argv =
   let rec parse = function
     | [] -> ()
    | "-impredicative-set" :: rem ->
@@ -340,7 +340,7 @@ let parse_args() =
     | s :: rem ->  add_compile s; parse rem
   in
   try
-    parse (List.tl (Array.to_list Sys.argv))
+    parse (List.tl (Array.to_list argv))
   with
     | UserError(_,s) as e -> begin
 	try
@@ -354,12 +354,12 @@ let parse_args() =
 (* To prevent from doing the initialization twice *)
 let initialized = ref false
 
-let init() =
+let init_with_argv argv =
   if not !initialized then begin
     initialized := true;
     Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
     try
-      parse_args();
+      parse_args argv;
       if_verbose print_header ();
       init_load_path ();
       engage ();
@@ -370,6 +370,8 @@ let init() =
       exit 1
   end
 
+let init() = init_with_argv Sys.argv
+
 let run () =
   try
     compile_files ();