From ca073a450f86c4ac109325d9037991852f72c7bf Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 9 Sep 2014 13:23:40 +0200
Subject: Load Prelude.vi if not Prelude.vo is found (Close: 3595)

---
 toplevel/coqtop.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 382a0185b8..c310986c61 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -117,7 +117,10 @@ let load_vernac_obj () =
 
 let require_prelude () =
   let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in
-  Library.require_library_from_dirpath [Coqlib.prelude_module,vo] (Some true)
+  let vi = Envars.coqlib () / "theories/Init/Prelude.vi" in
+  let m =
+    if Sys.file_exists vo then vo else if Sys.file_exists vi then vi else vo in
+  Library.require_library_from_dirpath [Coqlib.prelude_module,m] (Some true)
 
 let require_list = ref ([] : string list)
 let add_require s = require_list := s :: !require_list
-- 
cgit v1.2.3