Merge PR#479: [future] Remove unused parameter greedy.

7 files changed, 23 insertions, 24 deletions

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 130f1eb03..f147ea343 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -136,7 +136,7 @@ let dump (otab,_) =
   let disch_table = Array.make n a_discharge in
   let f2t_map = ref FMap.empty in
   Int.Map.iter (fun n (d,cu) ->
-    let c, u = Future.split2 ~greedy:true cu in
+    let c, u = Future.split2 cu in
     Future.sink u;
     Future.sink c;
     opaque_table.(n) <- c;
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3a0d1a2a5..a63eb3376 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -191,7 +191,7 @@ let infer_declaration ~trust env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) ->
+        Future.chain ~pure:true body (fun ((body,uctx),side_eff) ->
           let body, uctx, signatures =
             inline_side_effects env body uctx side_eff in
           let valid_signatures = check_signatures trust signatures in
@@ -416,7 +416,7 @@ let export_side_effects mb env ce =
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
       let ce = DefinitionEntry { c with
-        const_entry_body = Future.chain ~greedy:true ~pure:true body
+        const_entry_body = Future.chain ~pure:true body
           (fun (b_ctx, _) -> b_ctx, []) } in
       let not_exists (c,_,_,_) =
         try ignore(Environ.lookup_constant c env); false
@@ -498,7 +498,7 @@ let translate_local_def mb env id centry =
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
 let inline_entry_side_effects env ce = { ce with
-  const_entry_body = Future.chain ~greedy:true ~pure:true
+  const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
       (body, ctx'), []);
diff --git a/lib/future.ml b/lib/future.ml
index ea0382a63..b60b32bb6 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -191,9 +191,9 @@ let transactify f x =
 let purify_future f x = if is_over x then f x else purify f x
 let compute x = purify_future (compute ~pure:false) x
 let force ~pure x = purify_future (force ~pure) x
-let chain ?(greedy=true) ~pure x f =
+let chain ~pure x f =
   let y = chain ~pure x f in
-  if is_over x && greedy then ignore(force ~pure y);
+  if is_over x then ignore(force ~pure y);
   y
 let force x = force ~pure:false x
 
@@ -204,13 +204,13 @@ let join kx =
 
 let sink kx = if is_val kx then ignore(join kx)
 
-let split2 ?greedy x =
-  chain ?greedy ~pure:true x (fun x -> fst x),
-  chain ?greedy ~pure:true x (fun x -> snd x)
+let split2 x =
+  chain ~pure:true x (fun x -> fst x),
+  chain ~pure:true x (fun x -> snd x)
 
-let map2 ?greedy f x l =
+let map2 f x l =
   CList.map_i (fun i y ->
-    let xi = chain ?greedy ~pure:true x (fun x ->
+    let xi = chain ~pure:true x (fun x ->
         try List.nth x i
         with Failure _ | Invalid_argument _ ->
           CErrors.anomaly (Pp.str "Future.map2 length mismatch")) in
diff --git a/lib/future.mli b/lib/future.mli
index c780faf32..2a025ae84 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -113,8 +113,9 @@ val is_exn : 'a computation -> bool
 val peek_val : 'a computation -> 'a option
 val uuid : 'a computation -> UUID.t
 
-(* [chain greedy pure c f] chains computation [c] with [f].
- * The [greedy] and [pure] parameters are tricky:
+(* [chain pure c f] chains computation [c] with [f].
+ * [chain] forces immediately the new computation if the old one is_over (Exn or Val).
+ * The [pure] parameter is tricky:
  * [pure]:
  *   When pure is true, the returned computation will not keep a copy
  *   of the global state.
@@ -124,10 +125,8 @@ val uuid : 'a computation -> UUID.t
  *   one forces c' and then c''.
  *   [join c; chain ~pure:false c g] is invalid and fails at runtime.
  *   [force c; chain ~pure:false c g] is correct.
- * [greedy]:
- *   The [greedy] parameter forces immediately the new computation if
- *   the old one is_over (Exn or Val). Defaults to true. *)
-val chain : ?greedy:bool -> pure:bool ->
+ *)
+val chain : pure:bool ->
   'a computation -> ('a -> 'b) -> 'b computation
 
 (* Forcing a computation *)
@@ -143,9 +142,9 @@ val join : 'a computation -> 'a
 val sink : 'a computation -> unit
 
 (*** Utility functions ************************************************* ***)
-val split2 : ?greedy:bool ->
+val split2 :
   ('a * 'b) computation -> 'a computation * 'b computation
-val map2 : ?greedy:bool ->
+val map2 :
   ('a computation -> 'b -> 'c) ->
      'a list computation -> 'b list -> 'c list
 
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;
diff --git a/vernac/command.ml b/vernac/command.ml
index 049f58aa2..4b4f4d271 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -81,7 +81,7 @@ let red_constant_entry n ce sigma = function
         let Sigma (c, _, _) = redfun.e_redfun env sigma c in
         c
       in
-      { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out
+      { ce with const_entry_body = Future.chain ~pure:true proof_out
         (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
 
 let warn_implicits_in_term =
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 55f33be39..798a238c7 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -60,7 +60,7 @@ let adjust_guardness_conditions const = function
   (* Try all combinations... not optimal *)
      let env = Global.env() in
      { const with const_entry_body =
-        Future.chain ~greedy:true ~pure:true const.const_entry_body
+        Future.chain ~pure:true const.const_entry_body
         (fun ((body, ctx), eff) ->
           match kind_of_term body with
           | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->