From ca4b15c2ba733bdff783762bbfc4b53f88014320 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 20 May 2019 11:30:36 +0200
Subject: 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.
---
 kernel/opaqueproof.ml  | 7 -------
 kernel/opaqueproof.mli | 2 --
 2 files changed, 9 deletions(-)

(limited to 'kernel')

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
 
-- 
cgit v1.2.3