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.
iApply
theories/logrel/F_mu_ref_conc/binary/fundamental.v
done