Ticket #80 (closed bug: fixed)

Opened 4 years ago

Last modified 4 years ago

Alpha-renaming problem in samples/bugs/simple.spi

Reported by: hritcu Owned by: hritcu
Priority: critical Milestone: 0.2.1
Component: zk-typechecker Keywords:
Cc:

Description (last modified by hritcu) (diff)

The problem seems to be caused by "create_fresh_name" in alpha.ml, which checks the existence of the new name against a global list "used_name_list" and not against the given set "avoid". 

!!!3!!!fresh_name:m1
!!!4!!!dom f:anon6,c,dummy5,ks,m,m1,m2,y,yp,

Change History

comment:1 Changed 4 years ago by hritcu

  • Owner changed from somebody to hritcu
  • Status changed from new to assigned
  • Reporter changed from anonymous to hritcu

comment:2 Changed 4 years ago by hritcu

  • Summary changed from Alpha-renaming problem in bugs/simple.spi to Alpha-renaming problem in samples/bugs/simple.spi

comment:3 Changed 4 years ago by hritcu

  • Priority changed from major to critical
  • Description modified (diff)

comment:4 Changed 4 years ago by hritcu

  • Description modified (diff)

comment:5 Changed 4 years ago by hritcu

  • Description modified (diff)

comment:6 Changed 4 years ago by hritcu

  • Status changed from assigned to closed
  • Resolution set to fixed
Note: See TracTickets for help on using tickets.