Allow to delay polymorphic opaque constants.

We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.

4 files changed, 16 insertions, 11 deletions

diff --git a/library/global.ml b/library/global.ml
index 3f30a63808..44e4a9b7e1 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -139,9 +139,14 @@ let body_of_constant_body access env cb =
   | Undef _ | Primitive _ ->
      None
   | Def c ->
-     Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
+    let u = match cb.const_universes with
+    | Monomorphic _ -> Opaqueproof.PrivateMonomorphic ()
+    | Polymorphic _ -> Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty
+    in
+    Some (Mod_subst.force_constr c, u, Declareops.constant_polymorphic_context cb)
   | OpaqueDef o ->
-     Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb)
+    let c, u = Opaqueproof.force_proof access otab o in
+    Some (c, u, Declareops.constant_polymorphic_context cb)
 
 let body_of_constant_body access ce = body_of_constant_body access (env ()) ce
 
diff --git a/library/global.mli b/library/global.mli
index c36cec3511..34b6c52833 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -100,13 +100,16 @@ val mind_of_delta_kn : KerName.t -> MutInd.t
 
 val opaque_tables : unit -> Opaqueproof.opaquetab
 
-val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t ->
+  (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option
 (** Returns the body of the constant if it has any, and the polymorphic context
     it lives in. For monomorphic constant, the latter is empty, and for
     polymorphic constants, the term contains De Bruijn universe variables that
     need to be instantiated. *)
 
-val body_of_constant_body : Opaqueproof.indirect_accessor -> Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : Opaqueproof.indirect_accessor ->
+  Opaqueproof.opaque Declarations.constant_body ->
+    (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option
 (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
 
 (** {6 Compiled libraries } *)
diff --git a/library/library.ml b/library/library.ml
index 1ac75d2fdc..a55fe33617 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -280,7 +280,7 @@ type 'a table_status =
   | Fetched of 'a array
 
 let opaque_tables =
-  ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr option) table_status) LibraryMap.t)
+  ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t)
 
 let add_opaque_table dp st =
   opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -306,10 +306,7 @@ let access_table what tables dp i =
 
 let access_opaque_table dp i =
   let what = "opaque proofs" in
-  let (info, n, c) = access_table what opaque_tables dp i in
-  match c with
-  | None -> None
-  | Some c -> Some (Cooking.cook_constr info n c)
+  access_table what opaque_tables dp i
 
 let indirect_accessor = {
   Opaqueproof.access_proof = access_opaque_table;
@@ -323,7 +320,7 @@ type seg_sum = summary_disk
 type seg_lib = library_disk
 type seg_univ = (* true = vivo, false = vi *)
   Univ.ContextSet.t * bool
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
+type seg_proofs = Opaqueproof.opaque_proofterm array
 
 let mk_library sd md digests univs =
   {
diff --git a/library/library.mli b/library/library.mli
index 727eca10cf..de395fd3b4 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -35,7 +35,7 @@ type seg_sum
 type seg_lib
 type seg_univ = (* all_cst, finished? *)
   Univ.ContextSet.t * bool
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
+type seg_proofs = Opaqueproof.opaque_proofterm array
 
 (** Open a module (or a library); if the boolean is true then it's also
    an export otherwise just a simple import *)