Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."

This reverts commit c9c5412.

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.

Author: maximedenes

CHANGES

@@ -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.

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 <*>