Reduce the attack surface of Opaqueproof.

3 files changed, 11 insertions, 28 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4f992d3972..4fdd7ab334 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -608,11 +608,7 @@ let clean_bounded_mod_expr sign =
 (** {6 Stm machinery } *)
 let join_constant_body except otab cb =
   match cb.const_body with
-  | OpaqueDef o ->
-      (match Opaqueproof.uuid_opaque otab o with
-      | Some uuid when not(Future.UUIDSet.mem uuid except) ->
-          Opaqueproof.join_opaque otab o
-      | _ -> ())
+  | OpaqueDef o -> Opaqueproof.join_opaque ~except otab o
   | _ -> ()
 
 let join_structure except otab s =
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 303cb06c55..57059300b8 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -87,19 +87,18 @@ let discharge_direct_opaque ~cook_constr ci = function
   | Direct (d,cu) ->
       Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
 
-let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> ignore(Future.join cu)
+let join except cu = match except with
+| None -> ignore (Future.join cu)
+| Some except ->
+  if Future.UUIDSet.mem (Future.uuid cu) except then ()
+  else ignore (Future.join cu)
+
+let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
+  | Direct (_,cu) -> join except cu
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp then
         let fp = snd (Int.Map.find i prfs) in
-        ignore(Future.join fp)
-
-let uuid_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> Some (Future.uuid cu)
-  | Indirect (_,dp,i) ->
-      if DirPath.equal dp odp
-      then Some (Future.uuid (snd (Int.Map.find i prfs)))
-      else None
+        join except fp
 
 let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) ->
@@ -128,16 +127,6 @@ let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
       then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
       else !get_univ dp i
 
-let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> Future.chain cu fst
-  | Indirect (l,dp,i) ->
-      let pt =
-        if DirPath.equal dp odp
-        then Future.chain (snd (Int.Map.find i prfs)) fst
-        else !get_opaque dp i in
-      Future.chain pt (fun c ->
-        force_constr (List.fold_right subst_substituted l (from_val c)))
- 
 module FMap = Future.UUIDMap
 
 let a_constr = Future.from_val (mkRel 1)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 5ea6da649b..d47c0bbb3c 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -39,7 +39,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
     indirect opaque accessor configured below. *)
 val force_proof : opaquetab -> opaque -> constr
 val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
-val get_proof : opaquetab -> opaque -> constr Future.computation
 val get_constraints :
   opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
@@ -60,8 +59,7 @@ type cooking_info = {
 val discharge_direct_opaque :
   cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
 
-val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option
-val join_opaque : opaquetab -> opaque -> unit
+val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
 
 val dump : opaquetab ->
   Constr.t Future.computation array *