diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-20 14:01:05 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-20 14:01:05 +0100 |
| commit | fbd4464f4a43a714a6356db9caa704983190d212 (patch) | |
| tree | 89a1937e3f28baa23e2b579df6f13a30621acfc4 /stm/stm.ml | |
| parent | 75dad64e8c5d7c09145491518290bdb749b2d03c (diff) | |
| parent | 3502cc7c3bbad154dbfe76558d411d2c76109668 (diff) | |
Merge PR#479: [future] Remove unused parameter greedy.
Diffstat (limited to 'stm/stm.ml')
| -rw-r--r-- | stm/stm.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index e698d1c72..e56db4090 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1618,9 +1618,9 @@ end = struct (* {{{ *) Future.from_val (Option.get (Global.body_of_constant_body c)) in let uc = Future.chain - ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in - let pr = Future.chain ~greedy:true ~pure:true pr discharge in - let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in + ~pure:true uc Univ.hcons_universe_context_set in + let pr = Future.chain ~pure:true pr discharge in + let pr = Future.chain ~pure:true pr Constr.hcons in Future.sink pr; let extra = Future.join uc in u.(bucket) <- uc; |