-
Robbert Krebbers authored
Since strip_later is doing a good job stripping laters in the conclusion, these tactics are thus no longer needed. Also, wp_finish now properly converts the result in a primitive viewshift in case it is not a weakestpre.
eab6c6c4