-
Robbert Krebbers authored
By moving the later further to the outside, we can kill many occurences of `Next`, and get rid of laters/except_0s at awkward positions. Also we can have a sensible eliminator `proto_elim`.
51a90f82
By moving the later further to the outside, we can kill many occurences of `Next`, and get rid of laters/except_0s at awkward positions. Also we can have a sensible eliminator `proto_elim`.