rename: vi -> vio

2 files changed, 44 insertions, 42 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5e5d39ce6..2dcdc7bb7 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -159,9 +159,10 @@ let load_vernac_obj () =
 
 let require_prelude () =
   let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in
-  let vi = Envars.coqlib () / "theories/Init/Prelude.vi" in
+  let vio = Envars.coqlib () / "theories/Init/Prelude.vio" in
   let m =
-    if Sys.file_exists vo then vo else if Sys.file_exists vi then vi else vo in
+    if Sys.file_exists vo then vo else
+    if Sys.file_exists vio then vio else vo in
   Library.require_library_from_dirpath [Coqlib.prelude_module,m] (Some true)
 
 let require_list = ref ([] : string list)
@@ -333,45 +334,46 @@ let get_host_port opt s =
 
 let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
 
-let vi_tasks = ref []
+let vio_tasks = ref []
 
-let add_vi_task f =
+let add_vio_task f =
   set_batch_mode ();
   Flags.make_silent true;
-  vi_tasks := f :: !vi_tasks
+  vio_tasks := f :: !vio_tasks
 
-let check_vi_tasks () =
+let check_vio_tasks () =
   let rc =
-    List.fold_left (fun acc t -> Vi_checking.check_vi t && acc)
-      true (List.rev !vi_tasks) in
+    List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
+      true (List.rev !vio_tasks) in
   if not rc then exit 1
 
-let vi_files = ref []
-let vi_files_j = ref 0
-let vi_checking = ref false
-let add_vi_file f =
+let vio_files = ref []
+let vio_files_j = ref 0
+let vio_checking = ref false
+let add_vio_file f =
   set_batch_mode ();
   Flags.make_silent true;
-  vi_files := f :: !vi_files
-let set_vi_checking_j opt j =
-  try vi_files_j := int_of_string j
+  vio_files := f :: !vio_files
+
+let set_vio_checking_j opt j =
+  try vio_files_j := int_of_string j
   with Failure _ ->
     prerr_endline ("The first argument of " ^ opt ^ " must the number");
     prerr_endline "of concurrent workers to be used (a positive integer).";
     prerr_endline "Makefiles generated by coq_makefile should be called";
-    prerr_endline "setting the J variable like in 'make vi2vo J=3'";
+    prerr_endline "setting the J variable like in 'make vio2vo J=3'";
     exit 1
 
 let is_not_dash_option = function
   | Some f when String.length f > 0 && f.[0] <> '-' -> true
   | _ -> false
 
-let schedule_vi_checking () =
-  if !vi_files <> [] && !vi_checking then
-    Vi_checking.schedule_vi_checking !vi_files_j !vi_files
-let schedule_vi_compilation () =
-  if !vi_files <> [] && not !vi_checking then
-    Vi_checking.schedule_vi_compilation !vi_files_j !vi_files
+let schedule_vio_checking () =
+  if !vio_files <> [] && !vio_checking then
+    Vio_checking.schedule_vio_checking !vio_files_j !vio_files
+let schedule_vio_compilation () =
+  if !vio_files <> [] && not !vio_checking then
+    Vio_checking.schedule_vio_compilation !vio_files_j !vio_files
 
 let parse_args arglist =
   let args = ref arglist in
@@ -412,19 +414,19 @@ let parse_args arglist =
       end
 
     (* Options with two arg *)
-    |"-check-vi-tasks" ->
+    |"-check-vio-tasks" ->
         let tno = get_task_list (next ()) in
         let tfile = next () in
-        add_vi_task (tno,tfile)
-    |"-schedule-vi-checking" ->
-        vi_checking := true;
-        set_vi_checking_j opt (next ());
-        add_vi_file (next ());
-        while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done
-    |"-schedule-vi2vo" ->
-        set_vi_checking_j opt (next ());
-        add_vi_file (next ());
-        while is_not_dash_option (peek_next ()) do add_vi_file (next ()); done
+        add_vio_task (tno,tfile)
+    |"-schedule-vio-checking" ->
+        vio_checking := true;
+        set_vio_checking_j opt (next ());
+        add_vio_file (next ());
+        while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done
+    |"-schedule-vio2vo" ->
+        set_vio_checking_j opt (next ());
+        add_vio_file (next ());
+        while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done
 
     (* Options with one arg *)
     |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
@@ -461,7 +463,7 @@ let parse_args arglist =
     |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
     |"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
-    |"-vi2vo" -> add_compile false (next ()); Flags.compilation_mode := Vi2Vo
+    |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
     |"-toploop" -> toploop := Some (next ())
 
     (* Options with zero arg *)
@@ -494,7 +496,7 @@ let parse_args arglist =
     |"-output-context" -> output_context := true
     |"-q" -> no_load_rc ()
     |"-quiet"|"-silent" -> Flags.make_silent true
-    |"-quick" -> Flags.compilation_mode := BuildVi
+    |"-quick" -> Flags.compilation_mode := BuildVio
     |"-list-tags" -> print_tags := true
     |"-time" -> Flags.time := true
     |"-type-in-type" -> set_type_in_type ()
@@ -577,9 +579,9 @@ let init arglist =
       load_rcfile();
       load_vernacular ();
       compile_files ();
-      schedule_vi_checking ();
-      schedule_vi_compilation ();
-      check_vi_tasks ();
+      schedule_vio_checking ();
+      schedule_vio_compilation ();
+      check_vio_tasks ();
       outputstate ()
     with any ->
       let any = Errors.push any in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index e5c9849a9..682a06f78 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -326,20 +326,20 @@ let compile verbosely f =
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
       Dumpglob.end_dump_glob ()
-  | BuildVi ->
+  | BuildVio ->
       let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
       Dumpglob.noglob ();
       Stm.set_compilation_hints long_f_dot_v;
       let _ = load_vernac verbosely long_f_dot_v in
       Stm.finish ();
       check_pending_proofs ();
-      Stm.snapshot_vi ldir long_f_dot_v;
+      Stm.snapshot_vio ldir long_f_dot_v;
       Stm.reset_task_queue ()
-  | Vi2Vo ->
+  | Vio2Vo ->
       let open Filename in
       let open Library in
       Dumpglob.noglob ();
-      let f = if check_suffix f ".vi" then chop_extension f else f in
+      let f = if check_suffix f ".vio" then chop_extension f else f in
       let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
       Stm.set_compilation_hints lfdv;
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in