diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-04-25 17:04:33 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-04-25 17:09:22 +0200 |
| commit | 67b85b04d6d78d8e4bbec58eab4b0630abfcd67d (patch) | |
| tree | e60450476c561dca20af78d70fb3f9e8efc262af /kernel/opaqueproof.ml | |
| parent | 6e131a1e5d51af09b0c3163f2a32c9e47243af33 (diff) | |
Opaqueproofs: sink futures when interactive
Diffstat (limited to 'kernel/opaqueproof.ml')
| -rw-r--r-- | kernel/opaqueproof.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 50208e28a..102dcf99f 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -52,7 +52,7 @@ let turn_indirect o = match o with | Direct (d,cu) -> let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in match !mk_indirect (d,cu) with - | None -> NoIndirect([],cu) + | None -> Future.sink cu; NoIndirect([],cu) | Some (dp,i) -> Indirect ([],dp,i) let subst_opaque sub = function |