The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Hi Nadeem,

Le 7 mars 09 à 19:15, Nadeem Abdul Hamid a écrit :

> 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?

There's no way to do it yet. We should definitely have a "Print Opaque  
Dependencies"
to supplement "Print Assumptions". Consider it done!

-- Matthieu