From 78a03b8be4dc9603466bc22b6112113253f18765 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Thu, 30 Jan 2025 09:19:53 +0100 Subject: [PATCH] feat: load vos files We add the flag allowing the server to use vos files. --- language-server/vscoqtop/vscoqtop.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/language-server/vscoqtop/vscoqtop.ml b/language-server/vscoqtop/vscoqtop.ml index 84d78069..df0dcb27 100644 --- a/language-server/vscoqtop/vscoqtop.ml +++ b/language-server/vscoqtop/vscoqtop.ml @@ -45,6 +45,7 @@ let _ = let opts = Args.get_local_args cwd in let _injections = Coqinit.init_runtime opts in Safe_typing.allow_delayed_constants := true; (* Needed to delegate or skip proofs *) + Flags.load_vos_libraries := true; Sys.(set_signal sigint Signal_ignore); loop () [%%else] @@ -56,6 +57,7 @@ let () = let opts = Args.get_local_args cwd in let () = Coqinit.init_runtime ~usage:(Args.usage ()) opts in Safe_typing.allow_delayed_constants := true; (* Needed to delegate or skip proofs *) + Flags.load_vos_libraries := true; Sys.(set_signal sigint Signal_ignore); loop () [%%endif]