diff options
| author | Maxime Dénès | 2017-03-20 14:01:05 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-20 14:01:05 +0100 |
| commit | fbd4464f4a43a714a6356db9caa704983190d212 (patch) | |
| tree | 89a1937e3f28baa23e2b579df6f13a30621acfc4 /vernac | |
| parent | 75dad64e8c5d7c09145491518290bdb749b2d03c (diff) | |
| parent | 3502cc7c3bbad154dbfe76558d411d2c76109668 (diff) | |
Merge PR#479: [future] Remove unused parameter greedy.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 2 |
2 files changed, 2 insertions, 2 deletions
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)) -> |