Set the priority of the rewrite relation for sqsubseteq to not take precedence over... (!362) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Matthieu Sozeau requested to merge mattam82/stdpp:pr-13969-take3 into master 3 years ago

All threads resolved!

Set the priority of the rewrite relation for sqsubseteq to not take precedence over the eq instance from Coq or equiv.

Edited 3 years ago by Matthieu Sozeau

Activity

Matthieu Sozeau changed title from Set the priority of the rewrite relation for equiv to not take precedence over... to Set the priority of the rewrite relation for sqsubseteq to not take precedence over... 3 years ago

changed title from Set the priority of the rewrite relation for equiv to not take precedence over... to Set the priority of the rewrite relation for sqsubseteq to not take precedence over...
Matthieu Sozeau changed the description 3 years ago

changed the description
Matthieu Sozeau added 4 commits 3 years ago
added 4 commits

aaae68c7...607ee2b1 - 2 commits from branch iris:master

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

7ab55dc0 - Fix sqsubseteq_rewrite's priority, making it lower than equiv

Compare with previous version
Matthieu Sozeau added 1 commit 3 years ago
added 1 commit

36bc5009 - Fix sqsubseteq_rewrite's priority, making it lower than equiv

Compare with previous version
Matthieu Sozeau mentioned in merge request iris!773 (merged) 3 years ago

mentioned in merge request iris!773 (merged)
Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 3 years ago

Resolved 3 years ago by Robbert Krebbers
Last reply by Robbert Krebbers 3 years ago

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 3 years ago

Resolved 3 years ago by Robbert Krebbers

Matthieu Sozeau added 1 commit 3 years ago

added 1 commit

4bff5395 - Leave more room for priorities between equiv and sqsubseteq

Compare with previous version

Matthieu Sozeau added 1 commit 3 years ago

added 1 commit

4dd6ec09 - Leave more room for priorities between equiv and sqsubseteq

Compare with previous version

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 3 years ago

Resolved 3 years ago by Robbert Krebbers

Robbert Krebbers @robbertkrebbers started a thread on an old version of the diff 3 years ago

Resolved 3 years ago by Robbert Krebbers

Robbert Krebbers added 1 commit 3 years ago

added 1 commit

0eb7c546 - Apply 2 suggestion(s) to 1 file(s)

Compare with previous version

Robbert Krebbers resolved all threads 3 years ago

resolved all threads

Robbert Krebbers enabled an automatic merge when the pipeline for succeeds 3 years ago

enabled an automatic merge when the pipeline for 0eb7c546 succeeds

Robbert Krebbers @robbertkrebbers · 3 years ago

Owner

Merging, thanks.

Robbert Krebbers merged 3 years ago

merged

Robbert Krebbers mentioned in commit 3 years ago

mentioned in commit ac02dbbd

Please register or sign in to reply