iFresh should reserve fresh names
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.
iDestruct will also use
iFresh and gets a name that conflicts with
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.