aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli2
2 files changed, 2 insertions, 2 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 9832ba5876..91e28132ab 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -45,7 +45,7 @@ let boot = ref false
let batch_mode = ref false
-type compilation_mode = BuildVo | BuildVi
+type compilation_mode = BuildVo | BuildVi | Vi2Vo
let compilation_mode = ref BuildVo
type async_proofs = APoff | APonLazy | APonParallel of int
diff --git a/lib/flags.mli b/lib/flags.mli
index ecaa11388f..6c6aa5fbeb 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -11,7 +11,7 @@
val boot : bool ref
val batch_mode : bool ref
-type compilation_mode = BuildVo | BuildVi
+type compilation_mode = BuildVo | BuildVi | Vi2Vo
val compilation_mode : compilation_mode ref
type async_proofs = APoff | APonLazy | APonParallel of int