diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 24 |
1 files changed, 10 insertions, 14 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index d469994f3f..660dc27211 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1837,22 +1837,18 @@ 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 Library.indirect_accessor (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 Library.indirect_accessor c)) in + let pr = discharge pr in + let pr = Constr.hcons pr in + u.(bucket) <- Some uc; + p.(bucket) <- Some pr; + u, Univ.ContextSet.union cst uc, false let check_task name l i = match check_task_aux "" name l i with |