The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

I have a somewhat complicated fixpoint function that's been defined  
using Program, but in some parts of its definition I think I've ended  
up using opaque lemmas from the FSets library, so in certain cases the  
function doesn't reduce nicely to a simple result when I apply  
[compute]. So:

 - is there any easy way in general to determine what opaque  
definitions might have been used?
 - does anyway have any tips/tricks that they use in this sort of  
situation other than trying to identify the opaque lemmas and then  
essentially re-defining them as transparent?

Thanks,
--- nadeem