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`.
---
 vernac/command.ml | 2 +-
 vernac/lemmas.ml  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 049f58aa26..4b4f4d2711 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 55f33be399..798a238c74 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)) ->
-- 
cgit v1.2.3