diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-05 17:30:03 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-14 11:31:19 +0100 |
| commit | 3502cc7c3bbad154dbfe76558d411d2c76109668 (patch) | |
| tree | 7f336710bcf2d6399d7391a133acf57c9542ef0c /vernac/lemmas.ml | |
| parent | ecacc9af6100f76e95acc24e777026bfc9c4d921 (diff) | |
[future] Remove unused parameter greedy.
It was always set to `greedy:true`.
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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)) -> |