Put the old version of splitting back in

Only coq trunk supports -time, so we should keep an old version of
splitting around.