The Coq mailing list

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

Le 18 mars 09 à 08:00, Adam Koprowski a écrit :

   Hi Matthieu,

Hi Adam,

On Sun, Mar 8, 2009 at 02:57, Matthieu Sozeau <Matthieu.Sozeau AT lri.fr> wrote:

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

 
   I'd love to see that future! (figuring "by hand" what opaque definitions are in the way of reduction can be quite painful).

It's called "Print Opaque Dependencies" in the trunk and it does traverse 

opaque defs to find more opaque dependencies, so you get them all at once.

It'll probably be in the next 8.2 release.

-- Matthieu