1419.v « shouldsucceed « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/bugs/closed/shouldsucceed/1419.v

blob: d021107d1d52c2521f9331674be1f28a66f0c8a2 (plain)

Goal True.
  set(a := 0).
  set(b := a).
  unfold a in b.
  clear a.
  Eval vm_compute in  b.
  trivial.
Qed.