Keep sideconditions inside the iris ctx (!159) · Merge requests · Iris / RefinedC · GitLab

Michael Sammler requested to merge time/keep_sidecond_in_goal into master Jul 25, 2023

This is in preparation to keep existential quantifiers in the goal. It has even a small benefit for performance: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=f3820ba52a435b7f9afea16180514dde65b639f4&var-config1=build-coq.8.17.0-timing&var-branch2=time%2Fkeep_sidecond_in_goal&var-commit2=6946308078465f20d49245f3eb486eb60217afcd&var-config2=build-coq.8.17.0-timing&var-metric=instructions&var-group=%28.%2A%29