diff options
| author | Maxime Dénès | 2016-10-25 14:02:49 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-25 15:25:48 +0200 |
| commit | 9194180e2da0f7f9a2b2c7574bb7261cc69ead17 (patch) | |
| tree | 383054ef0da6cc80f3061c92b0db9cc462c2c512 /tactics | |
| 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')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 225ff3db94..549799974b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4589,7 +4589,7 @@ module New = struct let reduce_after_refine = Proofview.V82.tactic (reduce (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) - {onhyps=Some []; concl_occs=AllOccurrences }) + {onhyps=None; concl_occs=AllOccurrences }) let refine ?unsafe c = Proofview.Refine.refine ?unsafe c <*> |