Set the priority of the rewrite relation for equiv to not take precedence over...

Set the priority of the rewrite relation for equiv to not take precedence over the eq instance from Coq. This is more backwards compatible performance-wise with the old resolution where eq was favored (otherwise we get a 70% slowdown in perennial).

resolved all threads

added 1 commit

• 4a849876 - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

Thanks. LGTM. Merging.

enabled an automatic merge when the pipeline for 4a849876 succeeds

Unfortunately, I couldn't bench perennial before the previous PR was merged in stdpp + iris...

canceled the automatic merge

resolved all threads

added 1 commit

• 86140f3c - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

enabled an automatic merge when the pipeline for 86140f3c succeeds

I guess automatic merge failed while the pipeline succeeded.

canceled the automatic merge

resolved all threads

mentioned in commit 607ee2b1

merged

Thanks for catching that @mattam82. I was waiting for the merge email to update Iris (but that email never happened since something went wrong here...).

Iris has been updated to use a version of std++ that includes this MR.