Skip to content

Store a counter in `Envs` to assign fresh names with `iFresh`.

Joseph Tassarotti requested to merge joe/fresh into gen_proofmode

This addresses #170 (closed). I just did the simplest thing I could think of by threading a counter through through Envs. I do not add any invariants to envs_wf to guarantee that the current value in the counter is unused or anything.

So far I have only tested against the main Iris development.

Merge request reports