From 5bf25dfce23da1cee04b1c886e026f0dbc902c9c Mon Sep 17 00:00:00 2001
From: charguer
Date: Fri, 8 Nov 2019 11:06:10 +0100
Subject: From CoqIDE or -vos or -vok compilation, load .vo when .vos is
 missing (fixing bug #11057). With this new behavior, it is not needed to .vos
 files in user contribs. Also, this commit adds a feature: upon creation of a
 .vo file, an empty .vok file is touched.

---
 vernac/loadpath.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'vernac')

diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml
index b3dc254a63..a8462e31e1 100644
--- a/vernac/loadpath.ml
+++ b/vernac/loadpath.ml
@@ -140,12 +140,10 @@ let select_vo_file ~warn loadpath base =
     with Not_found -> None in
   if !Flags.load_vos_libraries then begin
     (* If the .vos file exists and is not empty, it describes the library.
-       If the .vos file exists and is empty, then load the .vo file.
-       If the .vos file is missing, then fail. *)
+       Otherwise, load the .vo file, or fail if is missing. *)
     match find ".vos" with
-    | None -> Error LibNotFound
-    | Some (_, vos as resvos) ->
-        if (Unix.stat vos).Unix.st_size > 0 then Ok resvos else
+    | Some (_, vos as resvos) when (Unix.stat vos).Unix.st_size > 0 -> Ok resvos
+    | _ ->
         match find ".vo" with
         | None -> Error LibNotFound
         | Some resvo -> Ok resvo
-- 
cgit v1.2.3