coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yves Bertot <Yves.Bertot AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] coq-dpdgraph release 0.6
- Date: Fri, 13 May 2016 08:09:12 +0200
On 05/11/2016 06:27 PM, Frédéric Blanqui wrote:
Hello Yves. Does dpdgraph print universe dependencies too?No, we did not think of it. The message "support for universe polymorphic constants" only expresses that the previous version would break in the presence of universe polymorphic constants.
My impression is that a program printing universe dependencies requires a completely different exploration of Coq's database. It must not be too hard to program, as long as we find the right entry points. Thanks for the suggestion.
Yves
- [Coq-Club] coq-dpdgraph release 0.6, Yves Bertot, 05/11/2016
- Re: [Coq-Club] coq-dpdgraph release 0.6, Frédéric Blanqui, 05/11/2016
- Re: [Coq-Club] coq-dpdgraph release 0.6, Yves Bertot, 05/13/2016
- Re: [Coq-Club] coq-dpdgraph release 0.6, Frédéric Blanqui, 05/11/2016
Archive powered by MHonArc 2.6.18.