Skip to content

Avoid relying on buggy simpl never behavior

Tej Chajed requested to merge tchajed/stdpp:simpl-never-fix into master

What's going on in this proof is that simpl is unfolding both decode_nat and decode, even though decode is marked simpl never. This is a bug in Coq and std++ should not rely on it.

Alternate take on, which is used as an overlay in Coq for

Merge request reports