The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello Yves. Does dpdgraph print universe dependencies too?

Le 11/05/2016 14:01, Yves Bertot a écrit :
> Dear all,
>
> We are pleased to announce a new release of coq-dpdgraph, a plugin and a
> set of tools to build depdency graphs between coq objects 
> (definitions, theorems, constructors).
>
> His new release compiles with Coq 8.5. The documentation is available at:
>
> https://github.com/karmaki/coq-dpdgraph
>
> It is also available on opam (in the Coq released suite).
>
> The changes brought by this release:
>
>   - support for universe polymorphic constants
>   - support for primitive projections
>   - improved documentation
>   - a tool call dpdusage to list constants that are never used by 
> other definitions (contribution of
>   Vadim Zaliva).
>
> Yves