Consider switching from simpl to cbn
I have the feeling we should try to switch to
cbnonce more. It solves at least the issue of over-eager unfolding, and the issue of not folding back.
Last time I tried, I ran into several other blockers, but maybe these are either fixed in Coq, or there are better workarounds than [what] we currently need to get
I agree; the only problems I'm aware of with
cbn are that:
- it crashes on 8.11.0 with mutual inductives, but that was fixed immediately, and 8.11.1 and .2 are out; it was due to a general refactoring.
- with ssreflect, you can write
simpla subterm matching a pattern) a but not
cbnthe same subterm).
Set SimplIsCbn would help with the latter, but it might be too strong (it didn't work for https://github.com/HoTT/HoTT/issues/709, never tried it myself, tho I probably should since I use Autosubst which is
cbn-based). I expect exporting
Set SimplIsCbn is probably best avoided.