From 72dc33fb0f99d403e8693db178a73c1e28096400 Mon Sep 17 00:00:00 2001
From: charguer
Date: Thu, 8 Nov 2018 16:50:13 +0100
Subject: Implementing support for vos/vok files.

A .vos file stores the result of compiling statements (defs, lemmas)
but not proofs.
A .vok file is an empty file that denotes successful compilation of
the full contents of a .v file.
Unlike a .vio file, a .vos file does not store suspended proofs,
so it is more lightweight. It cannot be completed into a .vo file.
---
 lib/flags.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index 7676665fe9..90b5f877d5 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -44,6 +44,8 @@ let with_options ol f x =
 let async_proofs_worker_id = ref "master"
 let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
 
+let load_vos_libraries = ref false
+
 let debug = ref false
 
 let in_debugger = ref false
-- 
cgit v1.2.3