Forked from
Iris / Iris
6565 commits behind the upstream repository.
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.
| Name | Last commit | Last update |
|---|---|---|
| .. | ||
| coq_tactics.v | ||
| environments.v | ||
| ghost_ownership.v | ||
| intro_patterns.v | ||
| invariants.v | ||
| notation.v | ||
| pviewshifts.v | ||
| spec_patterns.v | ||
| sts.v | ||
| tactics.v | ||
| weakestpre.v | ||