Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] coq-dpdgraph release 0.6

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coq-dpdgraph release 0.6


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page