diff options
| -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 8c0b140a85..f7baed0abe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4207,7 +4207,7 @@ module New = struct let reduce_after_refine = Proofview.V82.tactic (reduce (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) - {onhyps=None; concl_occs=AllOccurrences }) + {onhyps=Some[]; concl_occs=AllOccurrences }) let refine ?unsafe c = Proofview.Refine.refine ?unsafe c <*> |