rename: vi -> vio

5 files changed, 25 insertions, 25 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 1dff4ae94..4afdb06a1 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1145,7 +1145,7 @@ end = struct (* {{{ *)
     VCS.restore document;
     try
       Reach.known_state ~cache:`No stop;
-      (* The original terminator, a hook, has not been saved in the .vi*)
+      (* The original terminator, a hook, has not been saved in the .vio*)
       Proof_global.set_terminator
         (Lemmas.standard_proof_terminator []
           (Lemmas.mk_hook (fun _ _ -> ())));
@@ -1245,7 +1245,7 @@ end = struct (* {{{ *)
     let id, valid as t_exn_info = exn_info in
     let cancel_switch = ref false in
     if TaskQueue.n_workers (Option.get !queue) = 0 then
-      if !Flags.compilation_mode = Flags.BuildVi then begin
+      if !Flags.compilation_mode = Flags.BuildVio then begin
         let f,assign =
           Future.create_delegate ~blocking:true (State.exn_on id ~valid) in
         let t_uuid = Future.uuid f in
@@ -1536,11 +1536,11 @@ let async_policy () =
   if interactive () = `Yes then
     (async_proofs_is_master () || !async_proofs_mode = Flags.APonLazy)
   else
-    (!compilation_mode = Flags.BuildVi || !async_proofs_mode <> Flags.APoff)
+    (!compilation_mode = Flags.BuildVio || !async_proofs_mode <> Flags.APoff)
 
 let delegate name =
   let time = get_hint_bp_time name in
-  time >= 1.0 || !Flags.compilation_mode = Flags.BuildVi
+  time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
 
 let collect_proof keep cur hd brkind id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
@@ -1579,7 +1579,7 @@ let collect_proof keep cur hd brkind id =
         `ASync (parent last,proof_using_ast last,accn,name,delegate name)
     | `Fork((_, hd', GuaranteesOpacity, ids), _) when
        has_proof_no_using last && not (State.is_cached (parent last)) &&
-       !Flags.compilation_mode = Flags.BuildVi ->
+       !Flags.compilation_mode = Flags.BuildVio ->
         assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
         (try
           let name, hint = name ids, get_hint_ctx loc  in
@@ -1903,10 +1903,10 @@ let handle_failure (e, info) vcs tty =
       VCS.print ();
       iraise (e, info)
 
-let snapshot_vi ldir long_f_dot_v =
+let snapshot_vio ldir long_f_dot_v =
   finish ();
   if List.length (VCS.branches ()) > 1 then
-    Errors.errorlabstrm "stm" (str"Cannot dump a vi with open proofs");
+    Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
   Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v
     (Global.opaque_tables ())
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 715997aee..2cbd54dd5 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -49,18 +49,18 @@ val stop_worker : string -> unit
 (* Joins the entire document.  Implies finish, but also checks proofs *)
 val join : unit -> unit
 
-(* Saves on the dist a .vi corresponding to the current status:
+(* Saves on the dist a .vio corresponding to the current status:
    - if the worker prool is empty, all tasks are saved
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
      of the completed tasks is a failuere) *)
-val snapshot_vi : DirPath.t -> string -> unit
+val snapshot_vio : DirPath.t -> string -> unit
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
- * after having built a .vi in batch mode *)
+ * after having built a .vio in batch mode *)
 val reset_task_queue : unit -> unit
 
-(* A .vi contains tasks to be completed *)
+(* A .vio contains tasks to be completed *)
 type tasks
 val check_task : string -> tasks -> int -> bool
 val info_tasks : tasks -> (string * float * int) list
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 2b5ff8c04..92b3a869a 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -9,4 +9,4 @@ CoqworkmgrApi
 AsyncTaskQueue
 Texmacspp
 Stm
-Vi_checking
+Vio_checking
diff --git a/stm/vi_checking.ml b/stm/vio_checking.ml
index 925a2a89e..3922af6e1 100644
--- a/stm/vi_checking.ml
+++ b/stm/vio_checking.ml
@@ -8,7 +8,7 @@
 
 open Util
 
-let check_vi (ts,f) =
+let check_vio (ts,f) =
   Dumpglob.noglob ();
   let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
   Stm.set_compilation_hints long_f_dot_v;
@@ -23,12 +23,12 @@ end
 
 module Pool = Map.Make(IntOT)
 
-let schedule_vi_checking j fs =
+let schedule_vio_checking j fs =
   if j < 1 then Errors.error "The number of workers must be bigger than 0";
   let jobs = ref [] in
   List.iter (fun f ->
     let f =
-      if Filename.check_suffix f ".vi" then Filename.chop_extension f
+      if Filename.check_suffix f ".vio" then Filename.chop_extension f
       else f in
     let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
     Stm.set_compilation_hints long_f_dot_v;
@@ -42,7 +42,7 @@ let schedule_vi_checking j fs =
   let pool : Worker.process Pool.t ref = ref Pool.empty in
   let rec filter_argv b = function
     | [] -> []
-    | "-schedule-vi-checking" :: rest -> filter_argv true rest
+    | "-schedule-vio-checking" :: rest -> filter_argv true rest
     | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
     | _ :: rest when b -> filter_argv b rest
     | s :: rest -> s :: filter_argv b rest in
@@ -81,7 +81,7 @@ let schedule_vi_checking j fs =
     let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in
     List.flatten
       (List.map (fun (f, tl) ->
-        "-check-vi-tasks" :: 
+        "-check-vio-tasks" :: 
         String.concat "," (List.map string_of_int tl) :: [f])
       (pack (List.sort cmp_job !what))) in
   let rc = ref 0 in
@@ -97,12 +97,12 @@ let schedule_vi_checking j fs =
   done;
   exit !rc
 
-let schedule_vi_compilation j fs =
+let schedule_vio_compilation j fs =
   if j < 1 then Errors.error "The number of workers must be bigger than 0";
   let jobs = ref [] in
   List.iter (fun f ->
     let f =
-      if Filename.check_suffix f ".vi" then Filename.chop_extension f
+      if Filename.check_suffix f ".vio" then Filename.chop_extension f
       else f in
     let paths = Loadpath.get_paths () in
     let _, long_f_dot_v =
@@ -118,7 +118,7 @@ let schedule_vi_compilation j fs =
   let pool : Worker.process Pool.t ref = ref Pool.empty in
   let rec filter_argv b = function
     | [] -> []
-    | "-schedule-vi2vo" :: rest -> filter_argv true rest
+    | "-schedule-vio2vo" :: rest -> filter_argv true rest
     | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
     | _ :: rest when b -> filter_argv b rest
     | s :: rest -> s :: filter_argv b rest in
@@ -127,7 +127,7 @@ let schedule_vi_compilation j fs =
   let make_job () =
     let f, t = List.hd !jobs in
     jobs := List.tl !jobs;
-    [ "-vi2vo"; f ] in
+    [ "-vio2vo"; f ] in
   let rc = ref 0 in
   while !jobs <> [] || Pool.cardinal !pool > 0 do
     while Pool.cardinal !pool < j && !jobs <> [] do
diff --git a/stm/vi_checking.mli b/stm/vio_checking.mli
index 65414eda4..fb1a0beca 100644
--- a/stm/vi_checking.mli
+++ b/stm/vio_checking.mli
@@ -6,8 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* [check_vi tasks file] checks the [tasks] stored in [file] *)
-val check_vi : int list * string -> bool
-val schedule_vi_checking : int -> string list -> unit
+(* [check_vio tasks file] checks the [tasks] stored in [file] *)
+val check_vio : int list * string -> bool
+val schedule_vio_checking : int -> string list -> unit
 
-val schedule_vi_compilation : int -> string list -> unit
+val schedule_vio_compilation : int -> string list -> unit