Add annotations to avoid evars (!70) · Merge requests · Iris / examples · GitLab

Snippets Groups Projects

Merged Quentin VERMANDE requested to merge Tragicus/examples:rocq19987 into master 2 months ago

All threads resolved!

There are a few iApply in theories/logrel/F_mu_ref_conc/binary/fundamental.v that introduce evars, which causes the subsequent dones to be very slow (~10s each). This was also very fragile to https://github.com/coq/coq/pull/19987.

Activity

Quentin VERMANDE added 1 commit 2 months ago
added 1 commit

e7841de1 - name mangling

Compare with previous version
Quentin VERMANDE added 1 commit 2 months ago
added 1 commit

6567ed5b - duplicate clear

Compare with previous version
Ralf Jung @jung started a thread on an old version of the diff 2 months ago

Resolved 3 weeks ago by Robbert Krebbers
Last reply by Ralf Jung 2 months ago

Ralf Jung @jung started a thread on an old version of the diff 2 months ago

Resolved 3 weeks ago by Robbert Krebbers

Quentin VERMANDE added 1 commit 3 weeks ago

added 1 commit

9e8701cd - seal bin_log_related

Compare with previous version

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

Resolved 3 weeks ago by Robbert Krebbers

Quentin VERMANDE added 1 commit 3 weeks ago

added 1 commit

85bd8b93 - split long lines

Compare with previous version

Robbert Krebbers resolved all threads 3 weeks ago

resolved all threads

Robbert Krebbers mentioned in commit 3 weeks ago

mentioned in commit a056e2e1

Robbert Krebbers merged 3 weeks ago

merged

Please register or sign in to reply