Avoid relying on buggy simpl never behavior (!228) · Merge requests · Iris / stdpp

Tej Chajed requested to merge tchajed/stdpp:simpl-never-fix into master Feb 11, 2021

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 https://gitlab.inria.fr/bertot/stdpp/-/commit/895121f919c6f1332f41f658ce7f850e391eb49e, which is used as an overlay in Coq for https://github.com/coq/coq/pull/13448.

Avoid relying on buggy simpl never behavior

Merge request reports