From 667dc05ce35d45303662598f1e6b1923631431f4 Mon Sep 17 00:00:00 2001
From: charguer
Date: Fri, 25 Oct 2019 13:52:31 +0200
Subject: a tentative patch to allow interactive session to load .vos files;
 (recall that the generation of a .vo files induces the creation of an empty
 .vos file.)

---
 toplevel/coqtop.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index eded9f4bcd..309f5b657a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -271,6 +271,8 @@ let init_document opts =
      state before we take the first snapshot. This was not
      guaranteed in the past, but now is thanks to the STM API.
   *)
+  (* Next line allows loading .vos files when in interactive mode *)
+  Flags.load_vos_libraries := true;
   let iload_path = build_load_path opts in
   let require_libs = require_libs opts in
   let stm_options = opts.config.stm_flags in
-- 
cgit v1.2.3