Merge PR #10362: Kernel-side delaying of polymorphic opaque constants

Reviewed-by: SkySkimmer
Reviewed-by: gares

3 files changed, 20 insertions, 18 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 918d8ce08e..2840fc9ad6 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -51,7 +51,7 @@ let pr_path sp =
 type compilation_unit_name = DirPath.t
 
 type seg_univ = Univ.ContextSet.t * bool
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr option) array
+type seg_proofs = Opaqueproof.opaque_proofterm array
 
 type library_t = {
   library_name : compilation_unit_name;
@@ -98,10 +98,7 @@ let access_opaque_table dp i =
     with Not_found -> assert false
   in
   assert (i < Array.length t);
-  let (info, n, c) = t.(i) in
-  match c with
-  | None -> None
-  | Some c -> Some (Cooking.cook_constr info n c)
+  t.(i)
 
 let access_discharge = Cooking.cook_constr
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 0684623a81..9b41fbcb7a 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -10,7 +10,7 @@ open Environ
 
 let indirect_accessor = ref {
   Opaqueproof.access_proof = (fun _ _ -> assert false);
-  Opaqueproof.access_discharge = (fun _ _ _ -> assert false);
+  Opaqueproof.access_discharge = (fun _ _ -> assert false);
 }
 
 let set_indirect_accessor f = indirect_accessor := f
@@ -31,16 +31,19 @@ let check_constant_declaration env kn cb =
   in
   let ty = cb.const_type in
   let _ = infer_type env' ty in
-  let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with
-    | None, _ -> env'
-    | Some local, (OpaqueDef _, true) -> push_subgraph local env'
-    | Some _, _ -> assert false
-  in
-  let otab = Environ.opaque_tables env in
-  let body = match cb.const_body with
-  | Undef _ | Primitive _ -> None
-  | Def c -> Some (Mod_subst.force_constr c)
-  | OpaqueDef o -> Some (Opaqueproof.force_proof !indirect_accessor otab o)
+  let otab = Environ.opaque_tables env' in
+  let body, env' = match cb.const_body with
+  | Undef _ | Primitive _ -> None, env'
+  | Def c -> Some (Mod_subst.force_constr c), env'
+  | OpaqueDef o ->
+    let c, u = Opaqueproof.force_proof !indirect_accessor otab o in
+    let env' = match u, cb.const_universes with
+    | Opaqueproof.PrivateMonomorphic (), Monomorphic _ -> env'
+    | Opaqueproof.PrivatePolymorphic (_, local), Polymorphic _ ->
+      push_subgraph local env'
+    | _ -> assert false
+    in
+    Some c, env'
   in
   let () =
     match body with
diff --git a/checker/values.ml b/checker/values.ml
index 733c3db225..cde2db2721 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -230,7 +230,6 @@ let v_cb = v_tuple "constant_body"
     v_relevance;
     Any;
     v_univs;
-    Opt v_context_set;
     v_bool;
     v_typing_flags|]
 
@@ -399,6 +398,9 @@ let v_abstract =
 let v_cooking_info =
   Tuple ("cooking_info", [|v_work_list; v_abstract|])
 
-let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt v_constr |]))
+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_univopaques =
   Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))