The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

I'm trying to find a Set Printing setting that will visibly show the 
dependency mentioned by the error "Conclusion depends on the body of f" 
in the following goal at the point of the error.  Is there one?

Set Printing All.
Goal let f:=nat in let n:=0 in True.
intros f n.
change nat with f in n.
revert n.
(*At this point, the conclusion isn't _visibly_ dependent on f, let 
alone f's body*)
Fail clearbody f.

-- Jonathan