Skip to content
Snippets Groups Projects
Forked from Iris / Iris
Source project has a limited visibility.
  • Robbert Krebbers's avatar
    09b1563c
    Make iFresh faster on environments containing evars. · 09b1563c
    Robbert Krebbers authored
    Generating a fresh name consists of two stages:
    + Use [cbv] to compute a list representing the domain of the environment. This
      is a very simply computation that just erases the hypotheses.
    + Use [vm_compute] to compute a fresh name based on the list representing the
      domain. The domain itself should never contain evars, so [vm_compute] will
      do the job.
    09b1563c
    History
    Make iFresh faster on environments containing evars.
    Robbert Krebbers authored
    Generating a fresh name consists of two stages:
    + Use [cbv] to compute a list representing the domain of the environment. This
      is a very simply computation that just erases the hypotheses.
    + Use [vm_compute] to compute a fresh name based on the list representing the
      domain. The domain itself should never contain evars, so [vm_compute] will
      do the job.