Merge PR #10818: Merge Direct and Indirect nodes in Opaqueproof.

Reviewed-by: gares

4 files changed, 22 insertions, 24 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)
diff --git a/checker/values.ml b/checker/values.ml
index 6b340635d7..9a2028a96b 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -187,10 +187,24 @@ let v_substituted v_a =
 
 let v_cstr_subst = v_substituted v_constr
 
-(** NB: Second constructor [Direct] isn't supposed to appear in a .vo *)
-let v_lazy_constr =
-  v_sum "lazy_constr" 0 [|[|List v_subst;v_dp;Int|]|]
+let v_ndecl = v_sum "named_declaration" 0
+    [| [|v_binder_annot v_id; v_constr|];               (* LocalAssum *)
+       [|v_binder_annot v_id; v_constr; v_constr|] |]   (* LocalDef *)
+
+let v_nctxt = List v_ndecl
+
+let v_work_list =
+  let v_abstr = v_pair v_instance (Array v_id) in
+  Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|])
+
+let v_abstract =
+  Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |])
 
+let v_cooking_info =
+  Tuple ("cooking_info", [|v_work_list; v_abstract|])
+
+let v_opaque =
+  v_sum "opaque" 0 [|[|List v_subst; List v_cooking_info; v_dp; Int|]|]
 
 (** kernel/declarations *)
 
@@ -216,7 +230,7 @@ let v_primitive =
 
 let v_cst_def =
   v_sum "constant_def" 0
-    [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]; [|v_primitive|]|]
+    [|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|]
 
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool; v_bool|]
@@ -400,25 +414,9 @@ let v_libsum =
 let v_lib =
   Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
 
-let v_ndecl = v_sum "named_declaration" 0
-    [| [|v_binder_annot v_id; v_constr|];               (* LocalAssum *)
-       [|v_binder_annot v_id; v_constr; v_constr|] |]   (* LocalDef *)
-
-let v_nctxt = List v_ndecl
-
-let v_work_list =
-  let v_abstr = v_pair v_instance (Array v_id) in
-  Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|])
-
-let v_abstract =
-  Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |])
-
-let v_cooking_info =
-  Tuple ("cooking_info", [|v_work_list; v_abstract|])
-
 let v_delayed_universes =
   Sum ("delayed_universes", 0, [| [| v_unit |]; [| Int; v_context_set |] |])
 
-let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Opt (v_pair v_constr v_delayed_universes) |]))
+let v_opaquetable = Array (Opt (v_pair v_constr v_delayed_universes))
 let v_univopaques =
   Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))
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
diff --git a/checker/votour.ml b/checker/votour.ml
index f0e0cf22ab..5a610e6938 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -366,7 +366,7 @@ let visit_vo f =
     make_seg "univ constraints of opaque proofs" Values.v_univopaques;
     make_seg "discharging info" (Opt Any);
     make_seg "STM tasks" (Opt Values.v_stm_seg);
-    make_seg "opaque proofs" Values.v_opaques;
+    make_seg "opaque proofs" Values.v_opaquetable;
   |] in
   let repr =
     if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S)