aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/coqbugs0266.v
blob: cc3f307a206eb42cb5f7bc50b620c88b1a3f9f9e (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.
Fail clear a.