aboutsummaryrefslogtreecommitdiff
path: root/checker/values.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/values.mli')
-rw-r--r--checker/values.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/values.mli b/checker/values.mli
index 93983eb700..db6b0be250 100644
--- a/checker/values.mli
+++ b/checker/values.mli
@@ -46,5 +46,5 @@ type value =
val v_univopaques : value
val v_libsum : value
val v_lib : value
-val v_opaques : value
+val v_opaquetable : value
val v_stm_seg : value