diff options
| author | Maxime Dénès | 2019-10-12 13:28:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-10-12 13:28:35 +0200 |
| commit | cc4cddda2eb2a05f685c8404e4864ea0bcdac6eb (patch) | |
| tree | 134dc9c5bb95fd26789556231f73c69896b5255f /checker/check.ml | |
| parent | e8d0b5a8856a695dc3f6a28e2d305c095ef50c19 (diff) | |
| parent | 69551b566a1339543967a41ff4aaa4580e7394fc (diff) | |
Merge PR #10818: Merge Direct and Indirect nodes in Opaqueproof.
Reviewed-by: gares
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) |