From ecda2159a3c3176fb871bbc27b7c6b56d9f0830c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 20 Dec 2013 18:02:19 +0100
Subject: .vi files: .vo files without proofs

File format:
 The .vo file format changed:
   - after the magic number there are 3 segments. A segment is made of 3
     components: bynary int, an ocaml value, a digest.  The binary int
     is the position of the digest, so that one can skip the value without
     unmarshalling it
   - the first segment is the library, as before
   - the second segment is the STM task list
   - the third segment is the opaque table, as before
 A .vo file has a complete opaque table (all proof terms are there).
 A .vi file follows the same format of a .vo file, but some entries
 in the opaque table are missing.  A proof task is stocked instead.

Utilities:
 coqc: option -quick generates a .vi insted of a .vo
 coq_makefile: target quick to generate all .vi
 coqdep: generate deps for .vi files too
 votour: can browse .vi files too, the first question is which segment
         should be read
 coqchk: rejects .vi files
---
 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 b79f80d22f..0cefc90c4b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -45,6 +45,8 @@ let boot = ref false
 
 let batch_mode = ref false
 
+type compilation_mode = BuildVo | BuildVi
+let compilation_mode = ref BuildVo
 let coq_slave_mode = ref (-1)
 let coq_slaves_number = ref 1
 
-- 
cgit v1.2.3