diff options
| -rw-r--r-- | toplevel/stm.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 12c5cafd7f..17a5b13313 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -892,11 +892,13 @@ end = struct (* {{{ *) match c.Declarations.const_body with | Declarations.OpaqueDef lc -> let uc = Option.get (Opaqueproof.get_constraints lc) in + let uc = + Future.chain ~greedy:true ~pure:true uc Univ.hcons_constraints in let pr = Opaqueproof.get_proof lc in let pr = Future.chain ~greedy:true ~pure:true pr discharge in let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in - ignore(Future.join pr); - ignore(Future.join uc); + Future.sink pr; + Future.sink uc; u.(bucket) <- uc; p.(bucket) <- pr | _ -> assert false |