7 files changed, 23 insertions, 28 deletions

diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index 60c8fb4449..b241fdc6cc 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -21,7 +21,7 @@ val contents : aux_file -> string M.t H.t
 
 val aux_file_name_for : string -> string
 val start_aux_file : aux_file:string -> v_file:string -> unit
-val stop_aux_file : unit -> unit 
+val stop_aux_file : unit -> unit
 val recording : unit -> bool
 
 val record_in_aux_at : ?loc:Loc.t -> string -> string -> unit
diff --git a/lib/feedback.mli b/lib/feedback.mli
index dc8449ed71..5375d97d57 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -74,13 +74,8 @@ val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_conte
 (** [set_id_for_feedback route id] Set the defaults for feedback *)
 val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit
 
-(** {6 output functions}
+(** {6 output functions} *)
 
-[msg_notice] do not put any decoration on output by default. If
-possible don't mix it with goal output (prefer msg_info or
-msg_warning) so that interfaces can dispatch outputs easily. Once all
-interfaces use the xml-like protocol this constraint can be
-relaxed. *)
 (* Should we advertise these functions more? Should they be the ONLY
    allowed way to output something? *)
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 190de5853d..90b5f877d5 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -41,11 +41,11 @@ let with_options ol f x =
     let () = List.iter2 (:=) ol vl in
     Exninfo.iraise reraise
 
-let record_aux_file = ref false
-
 let async_proofs_worker_id = ref "master"
 let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
 
+let load_vos_libraries = ref false
+
 let debug = ref false
 
 let in_debugger = ref false
@@ -62,7 +62,7 @@ let we_are_parsing = ref false
 (* Current means no particular compatibility consideration.
    For correct comparisons, this constructor should remain the last one. *)
 
-type compat_version = V8_8 | V8_9 | Current
+type compat_version = V8_8 | V8_9 | V8_10 | Current
 
 let compat_version = ref Current
 
@@ -73,6 +73,9 @@ let version_compare v1 v2 = match v1, v2 with
   | V8_9, V8_9 -> 0
   | V8_9, _ -> -1
   | _, V8_9 -> 1
+  | V8_10, V8_10 -> 0
+  | V8_10, _ -> -1
+  | _, V8_10 -> 1
   | Current, Current -> 0
 
 let version_strictly_greater v = version_compare !compat_version v > 0
@@ -81,6 +84,7 @@ let version_less_or_equal v = not (version_strictly_greater v)
 let pr_version = function
   | V8_8 -> "8.8"
   | V8_9 -> "8.9"
+  | V8_10 -> "8.10"
   | Current -> "current"
 
 (* Translate *)
diff --git a/lib/flags.mli b/lib/flags.mli
index 1c96796220..76a78e61fc 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -31,14 +31,14 @@
 
 (** Command-line flags  *)
 
-(** Set by coqtop to tell the kernel to output to the aux file; will
-    be eventually removed by cleanups such as PR#1103 *)
-val record_aux_file : bool ref
-
 (** Async-related flags *)
 val async_proofs_worker_id : string ref
 val async_proofs_is_worker : unit -> bool
 
+(** Flag to indicate that .vos files should be loaded for dependencies
+    instead of .vo files. Used by -vos and -vok options. *)
+val load_vos_libraries : bool ref
+
 (** Debug flags *)
 val debug : bool ref
 val in_debugger : bool ref
@@ -52,7 +52,7 @@ val we_are_parsing : bool ref
 (* Set Printing All flag. For some reason it is a global flag *)
 val raw_print : bool ref
 
-type compat_version = V8_8 | V8_9 | Current
+type compat_version = V8_8 | V8_9 | V8_10 | Current
 val compat_version : compat_version ref
 val version_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
diff --git a/lib/future.ml b/lib/future.ml
index 01fb7d0297..d3ea538549 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -98,7 +98,6 @@ let peek_val kx = let _, _, _, x = get kx in match !x with
 let uuid kx = let _, id, _, _ = get kx in id
 
 let from_val ?(fix_exn=id) v = create fix_exn (Val v)
-let from_here ?(fix_exn=id) v = create fix_exn (Val v)
 
 let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
 
@@ -168,8 +167,6 @@ let join kx =
   kx := Finished v;
   v
 
-let sink kx = if is_val kx then ignore(join kx)
-
 let split2 x =
   chain x (fun x -> fst x), chain x (fun x -> snd x)
 
diff --git a/lib/future.mli b/lib/future.mli
index 8e5f704837..c0fc91bcc3 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -55,10 +55,6 @@ val create : fix_exn -> (unit -> 'a) -> 'a computation
    argument should really be given *)
 val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
 
-(* Like from_val, but also takes a snapshot of the global state.  Morally
-   the value is not just the 'a but also the global system state *)
-val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
-
 (* To get the fix_exn of a computation and build a Lemmas.declaration_hook.
  * When a future enters the environment a corresponding hook is run to perform
  * some work.  If this fails, then its failure has to be annotated with the
@@ -100,9 +96,6 @@ val compute : 'a computation -> 'a value
  * in a computation obtained by chaining on a joined future. *)
 val join : 'a computation -> 'a
 
-(* Call this before stocking the future.  If it is_val then it is joined *)
-val sink : 'a computation -> unit
-
 (*** Utility functions ************************************************* ***)
 val split2 :
   ('a * 'b) computation -> 'a computation * 'b computation
diff --git a/lib/system.ml b/lib/system.ml
index 46b358f825..8c333ec267 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -53,8 +53,14 @@ module StrSet = Set.Make(StrMod)
 let dirmap = ref StrMap.empty
 
 let make_dir_table dir =
+  let entries =
+    try
+      Sys.readdir dir
+    with Sys_error _ ->
+      warn_cannot_open_dir dir;
+      [||] in
   let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
-  Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir)
+  Array.fold_left filter_dotfiles StrSet.empty entries
 
 (** Don't trust in interactive mode (the default) *)
 let trust_file_cache = ref false
@@ -294,13 +300,13 @@ let with_time ~batch ~header f x =
     let y = f x in
     let tend = get_time() in
     let msg2 = if batch then "" else " (successful)" in
-    Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
     y
   with e ->
     let tend = get_time() in
     let msg = if batch then "" else "Finished failing transaction in " in
     let msg2 = if batch then "" else " (failure)" in
-    Feedback.msg_info (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
+    Feedback.msg_notice (header ++ str msg ++ fmt_time_difference tstart tend ++ str msg2);
     raise e
 
 (* We use argv.[0] as we don't want to resolve symlinks *)