diff options
| -rw-r--r-- | kernel/opaqueproof.ml | 7 | ||||
| -rw-r--r-- | kernel/opaqueproof.mli | 2 | ||||
| -rw-r--r-- | stm/stm.ml | 29 |
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 |