From 3502cc7c3bbad154dbfe76558d411d2c76109668 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 5 Mar 2017 17:30:03 +0100 Subject: [future] Remove unused parameter greedy. It was always set to `greedy:true`. --- stm/stm.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'stm/stm.ml') 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; -- cgit v1.2.3