simplify_eq fails under Coq 8.14
When porting Simuliris to Coq 8.14, simplify_eq started to fail in several places saying
Error: Not a negated primitive equality.
To reproduce, try building Simuliris with Coq 8.14; the error occurs in ./theories/stacked_borrows/steps_progress.v
, specifically at
- https://gitlab.mpi-sws.org/iris/simuliris/-/blob/87a3f6b/theories/stacked_borrows/steps_progress.v#L167
- once I fixed that with a manual proof, I got the same error again in https://gitlab.mpi-sws.org/iris/simuliris/-/blob/87a3f6b/theories/stacked_borrows/steps_progress.v#L239