iFresh should reserve fresh names
Right now iFresh
just generates a name that is fresh with respect to the current context, but doesn't ensure that the generated name will not be returned again by subsequent calls to iFresh
. As a result, the following pattern fails:
let H1 := iFresh in
let H2 := eval vm_compute in (match H1 with
| IAnon x => IAnon (1 + x)
| INamed x => IAnon 1
end) in
let pat :=constr:(IList [cons (IIdent H1) (cons (IIdent H2) nil)]) in
iDestruct "H" as pat.
because iDestruct
will also use iFresh
and gets a name that conflicts with H1
.
One solution would be to add a counter to the envs
record which is incremented each time iFresh
is called. This would actually also probably make iFresh
more efficient anyway.