aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-10-25 14:02:49 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-10-25 15:25:48 +0200
commit9194180e2da0f7f9a2b2c7574bb7261cc69ead17 (patch)
tree383054ef0da6cc80f3061c92b0db9cc462c2c512 /library
parent67b49d4d5afdd67bb0a81e3fdf6876387d28a36e (diff)
Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."
This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6. This behavior of refine has changed three times in recent years, so let's take the time to make up our mind and wait for a major release. Btw, onhyps=None is not a sane way to express that a tactic should be applied to all hypotheses.
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions