aboutsummaryrefslogtreecommitdiff
path: root/lib/flags.mli
diff options
context:
space:
mode:
authorEnrico Tassi2015-01-06 18:09:26 +0100
committerEnrico Tassi2015-01-06 18:09:35 +0100
commit341909bbc5c1c59e81dfad2f2532602e2561ec36 (patch)
tree28fb527cb921b4e02d4722549a24f6e2366f5c76 /lib/flags.mli
parentbf16900f43c1291136673e7614587fe51eebc88f (diff)
rename: vi -> vio
Diffstat (limited to 'lib/flags.mli')
-rw-r--r--lib/flags.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/flags.mli b/lib/flags.mli
index fbb2f817a6..c35943e53c 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -12,7 +12,7 @@ val boot : bool ref
val load_init : bool ref
val batch_mode : bool ref
-type compilation_mode = BuildVo | BuildVi | Vi2Vo
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
val compilation_mode : compilation_mode ref
type async_proofs = APoff | APonLazy | APon