diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-10-25 14:02:49 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-10-25 15:25:48 +0200 |
| commit | 9194180e2da0f7f9a2b2c7574bb7261cc69ead17 (patch) | |
| tree | 383054ef0da6cc80f3061c92b0db9cc462c2c512 /tactics/tacinterp.ml | |
| parent | 67b49d4d5afdd67bb0a81e3fdf6876387d28a36e (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 'tactics/tacinterp.ml')
0 files changed, 0 insertions, 0 deletions