diff options
| author | Pierre-Marie Pédrot | 2019-05-20 11:30:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-24 09:00:10 +0200 |
| commit | ca4b15c2ba733bdff783762bbfc4b53f88014320 (patch) | |
| tree | 6e4ee88413dc99d34c563ecdcac165d18920dd91 /kernel | |
| parent | 26169d33b45aae8bf2dfafa2b400a9780c73ea13 (diff) | |
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.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/opaqueproof.ml | 7 | ||||
| -rw-r--r-- | kernel/opaqueproof.mli | 2 |
2 files changed, 0 insertions, 9 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 |