diff options
Diffstat (limited to 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/check.ml b/checker/check.ml index 69de2536c5..09ecd675f7 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -359,7 +359,7 @@ let intern_from_file ~intern_mode (dir, f) = (* Verification of the unmarshalled values *) validate !Flags.debug Values.v_libsum sd; validate !Flags.debug Values.v_lib md; - validate !Flags.debug Values.(Opt v_opaques) table; + validate !Flags.debug Values.(Opt v_opaquetable) table; Flags.if_verbose chk_pp (str" done]" ++ fnl ()); let digest = if opaque_csts <> None then Safe_typing.Dvivo (digest,udg) |