Skip to content
Snippets Groups Projects
Forked from Iris / Iris
Source project has a limited visibility.
user avatar
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
Name Last commit Last update