diff options
| author | Enrico Tassi | 2014-03-03 14:39:25 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-03-04 17:35:58 +0100 |
| commit | 0ea9b2f2a972d49844a6e784d2cf19feb4dc7636 (patch) | |
| tree | 0207db227374dae92e4332f67054e299d8698f0a | |
| parent | 19688fcd1b99dae377f908529d3fed3804e95068 (diff) | |
STM: when finish a task hcons universe constraints
| -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 |