Remove the delayed universe table from object files.

This was virtually dead code. The only place really accessing this data was the
user pretty-printer, but actually the tables were not installed for vanilla vo
files.

In practice, that meant that the only case where an access to this table could
have been triggered would have been to print a term coming from a vio file,
or a vo file generated via vio2vo. In all other cases, the printer would not
have displayed the internal universes. While the latter might be considered
a bug, I am instead convinced that this notion of user-facing internal universes
needs to be handled by another mechanism, the current one making little sense.
The fact it was broken all along without anybody noticing proves my point.

2 files changed, 4 insertions, 11 deletions

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 0ff27eb4ea..1971c67c61 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -18,7 +18,6 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
 
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> constr option;
-  access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
 }
 
 type cooking_info = { 
@@ -107,14 +106,12 @@ let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
-let force_constraints access { opaque_val = prfs; opaque_dir = odp; _ } = function
+let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) -> snd(Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then snd (Future.force (snd (Int.Map.find i prfs)))
-      else match access.access_constraints dp i with
-        | None -> Univ.ContextSet.empty
-        | Some u -> u
+      else Univ.ContextSet.empty
 
 let get_direct_constraints = function
 | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
@@ -124,15 +121,13 @@ module FMap = Future.UUIDMap
 
 let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
   let opaque_table = Array.make n None in
-  let univ_table = Array.make n None in
   let disch_table = Array.make n [] in
   let f2t_map = ref FMap.empty in
   let iter n (d, cu) =
     let uid = Future.uuid cu in
     let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
     if Future.is_val cu then
-      let (c, u) = Future.force cu in
-      let () = univ_table.(n) <- Some u in
+      let (c, _) = Future.force cu in
       opaque_table.(n) <- Some c
     else if Future.UUIDSet.mem uid except then
       disch_table.(n) <- d
@@ -141,4 +136,4 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
         Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
   in
   let () = Int.Map.iter iter otab in
-  opaque_table, univ_table, disch_table, !f2t_map
+  opaque_table, disch_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 4646206e55..46b0500507 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -37,7 +37,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 
 type indirect_accessor = {
   access_proof : DirPath.t -> int -> constr option;
-  access_constraints : DirPath.t -> int -> Univ.ContextSet.t option;
 }
 (** When stored indirectly, opaque terms are indexed by their library
     dirpath and an integer index. The two functions above activate
@@ -70,6 +69,5 @@ val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : ?except:Future.UUIDSet.t -> opaquetab ->
   Constr.t option array *
-  Univ.ContextSet.t option array *
   cooking_info list array *
   int Future.UUIDMap.t