From 69551b566a1339543967a41ff4aaa4580e7394fc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 26 Sep 2019 17:02:26 +0200
Subject: Merge Direct and Indirect nodes in Opaqueproof.

---
 checker/check.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker/check.ml')

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)
-- 
cgit v1.2.3