diff options
| -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 225ff3db9..549799974 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 <*> |