Skip to content

Add annotations to avoid evars

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.

Merge request reports

Loading