Remove a useless call to the Future API for opaque proofs in the STM.

We know statically that the check function producing this forces its
argument, so there is no point in chaining futures lazily.

3 files changed, 15 insertions, 23 deletions

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index d168f3cb7e..5584b74b36 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -119,13 +119,6 @@ let get_direct_constraints = function
 | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
 | Direct (_, cu) -> Future.chain cu snd
 
-let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
-  | Direct (_,cu) -> Some(Future.chain cu snd)
-  | Indirect (_,dp,i) ->
-      if DirPath.equal dp odp
-      then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
-      else !get_univ dp i
-
 module FMap = Future.UUIDMap
 
 let a_constr = Future.from_val (mkRel 1)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 501779a917..b84aeaf35a 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -40,8 +40,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 val force_proof : opaquetab -> opaque -> constr
 val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
 val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
-val get_constraints :
-  opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
 
 val subst_opaque : substitution -> opaque -> opaque
 
diff --git a/stm/stm.ml b/stm/stm.ml
index d469994f3f..9e9d23ba93 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1837,22 +1837,23 @@ end = struct (* {{{ *)
         let o = match c.Declarations.const_body with
           | Declarations.OpaqueDef o -> o
           | _ -> assert false in
-        let uc =
-          Option.get
-            (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
+        (* No need to delay the computation, the future has been forced by
+           the call to [check_task_aux] above. *)
+        let uc = Opaqueproof.force_constraints (Global.opaque_tables ()) o in
+        let uc = Univ.hcons_universe_context_set uc in
         (* We only manipulate monomorphic terms here. *)
         let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
-        let pr =
-          Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
-        let uc =
-          Future.chain uc Univ.hcons_universe_context_set in
-        let pr = Future.chain pr discharge in
-        let pr = Future.chain pr Constr.hcons in
-        Future.sink pr;
-        let extra = Future.join uc in
-        u.(bucket) <- uc;
-        p.(bucket) <- pr;
-        u, Univ.ContextSet.union cst extra, false
+        let pr = map (Option.get (Global.body_of_constant_body c)) in
+        let pr = discharge pr in
+        let pr = Constr.hcons pr in
+        let return c =
+          let fc = Future.from_val c in
+          let _ = Future.join fc in
+          fc
+        in
+        u.(bucket) <- return uc;
+        p.(bucket) <- return pr;
+        u, Univ.ContextSet.union cst uc, false
 
   let check_task name l i =
     match check_task_aux "" name l i with