diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-01-12 17:02:46 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-01-12 18:34:05 +0100 |
commit | ab1df17788e89d76c656a403850e9b2caa677cff (patch) | |
tree | af97e0a00488d0646ecff069a382a9b95c2f15ec /library | |
parent | bf142d5058c3767a9fae07f32e98ddbfd3720d1a (diff) |
fixup to vi -> vio renaming
Diffstat (limited to 'library')
-rw-r--r-- | library/library.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/library/library.ml b/library/library.ml index 690366d9a..78912dbbf 100644 --- a/library/library.ml +++ b/library/library.ml @@ -222,7 +222,7 @@ let locate_absolute_library dir = let _, file = System.where_in_path ~warn:false loadpath name in [file] with Not_found -> [] in - match find ".vo" @ find ".vi" with + match find ".vo" @ find ".vio" with | [] -> raise LibNotFound | [file] -> dir, file | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> @@ -245,7 +245,7 @@ let locate_qualified_library warn qid = [lpath, file] with Not_found -> [] in let lpath, file = - match find ".vo" @ find ".vi" with + match find ".vo" @ find ".vio" with | [] -> raise LibNotFound | [lpath, file] -> lpath, file | [lpath_vo, vo; lpath_vi, vi] @@ -623,7 +623,7 @@ let load_library_todo f = let paths = Loadpath.get_paths () in let _, longf = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in - let f = longf^"i" in + let f = longf^"io" in let ch = System.with_magic_number_check raw_intern_library f in let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in @@ -631,10 +631,10 @@ let load_library_todo f = let tasks, _, _ = System.marshal_in_segment f ch in let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in close_in ch; - if tasks = None then errorlabstrm "restart" (str"not a .vi file"); - if s2 = None then errorlabstrm "restart" (str"not a .vi file"); - if s3 = None then errorlabstrm "restart" (str"not a .vi file"); - if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vi file"); + if tasks = None then errorlabstrm "restart" (str"not a .vio file"); + if s2 = None then errorlabstrm "restart" (str"not a .vio file"); + if s3 = None then errorlabstrm "restart" (str"not a .vio file"); + if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file"); longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5 (************************************************************************) @@ -669,7 +669,7 @@ let save_library_to ?todo dir f otab = assert(!Flags.compilation_mode = Flags.BuildVo); f ^ "o", Future.UUIDSet.empty | Some (l,_) -> - f ^ "i", + f ^ "io", List.fold_left (fun e r -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty l in let cenv, seg, ast = Declaremods.end_library ~except dir in |