aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/ClearBody.v
blob: 609d5b3b0faf0b5ab4d053dea03f4ad6f07ff5a1 (plain)
1
2
3
4
5
6
7
8
(* ClearBody must check that removing the body of definition does not
   invalidate the well-typabilility of the visible goal *)

Goal True.
set (n := 0) in *.
set (I := refl_equal 0) in *.
change (n = 0) in (type of I).
clearbody n.