diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-22 13:43:56 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-22 13:44:57 +0200 |
| commit | 8afac4f87d9d7e3add1c19485f475bd2207bfde7 (patch) | |
| tree | 387fe00e0e2d828c04a68916fa57d027bbb29446 | |
| parent | c2bdd1d3145556423621223694bd9fb23fe86a64 (diff) | |
Refine tactic: simplify the conclusion only at the end of the tactic.
It was the intended semantics from the beginning. I just wrote it wrong.
Spotted by Hugo, fix by Hugo.
| -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 8c0b140a8..f7baed0ab 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 <*> |