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