test-suite/failure/ClearBody.v


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.
LetTac n:=O.
LetTac I:=(refl_equal nat O).
Change (n=O) in (Type of I).
ClearBody n.