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 | |
| 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.
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
2 files changed, 1 insertions, 2 deletions
@@ -24,7 +24,6 @@ Other bugfixes - #4156: micromega cache files are now hidden files. - #4871: interrupting par:abstract kills coqtop. - #5043: [Admitted] lemmas pick up section variables. -- Fix call to "lazy beta iota" in "refine" (restoring v8.4 behavior). - Fix name of internal refine ("simple refine"). - #5062: probably a typo in Strict Proofs mode. - #5065: Anomaly: Not a proof by induction. 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 <*> |