diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-23 20:48:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-24 16:44:48 +0200 |
| commit | 08e87eb96ab67ead60d92394eec6066d9b52e55e (patch) | |
| tree | 9a51bbbec185b601dd38bb7682347c5025c7b08b | |
| parent | f9386dc81a403e926908db7574702c0c566334e2 (diff) | |
Apparently, the former refine was simplifying in hypotheses too.
| -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 0b7edecac..0875a7656 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4202,7 +4202,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 <*> |