diff options
| author | Enrico Tassi | 2014-09-09 13:23:40 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-09 13:23:40 +0200 |
| commit | ca073a450f86c4ac109325d9037991852f72c7bf (patch) | |
| tree | b7c4bcf2eb3fd7d5beb1b6a1c0377e3fa798a8e2 | |
| parent | ba30a3da1f41aec6404b49832cdc8516fdcc78ec (diff) | |
Load Prelude.vi if not Prelude.vo is found (Close: 3595)
| -rw-r--r-- | toplevel/coqtop.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 |