Use more Hint Extern instead of IsEx (!161) · Merge requests · Iris / RefinedC · GitLab

Michael Sammler requested to merge time/more_hint_extern into master Jul 31, 2023

Not a big win, but probably still worth it: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=3ba9876efb0884f13fd3a01abb54cffbefa78cbb&var-config1=build-coq.8.17.0-timing&var-branch2=time%2Fmore_hint_extern&var-commit2=0960c81d01f651d1df4c18358bfd56a5351758f5&var-config2=build-coq.8.17.0-timing&var-metric=instructions&var-group=%28%29.%2A