coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Inaccurate [Print Universes]?

From: Stéphane Glondu <steph AT glondu.net>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Inaccurate [Print Universes]?
Date: Tue, 26 Jun 2012 08:47:13 +0200
Openpgp: id=49881AD3

Le 26/06/2012 04:44, Jason Gross a écrit :
> Is it possible for [Print Universes] to be wrong? [...]
> Is this a bug in [Print Universes] or in Coq's universe consistency
> checker, or am I mis-reading the output of [Print Universes]?

It is possible that it is a bug in Coq's universe consistency checker.
There have been bugs there in the past. What does "Print Sorted
Universes" do? What version are you using? It would be useful to answer
to these questions in a bugreport. It would also be useful to provide a
.v file that exhibits the behaviour.

Cheers,

--
Stéphane

[Coq-Club] Inaccurate [Print Universes]?, Jason Gross, 06/26/2012
- Re: [Coq-Club] Inaccurate [Print Universes]?, Stéphane Glondu, 06/26/2012
- Re: [Coq-Club] Inaccurate [Print Universes]?, Bruno Barras, 06/26/2012