aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/coqbugs0266.v
blob: 79eef5c92a02d01b5a5dc96ee16581897d64d892 (plain)
1
2
3
4
5
6
7
(* It is forbidden to erase a variable (or a local def) that is used in
   the current goal. *)
Section S.
Let a := 0.
Definition b := a.
Goal b = b.
clear a.