coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Rene Vestergaard <vester AT jaist.ac.jp>
To: Pierre Casteran <pierre.casteran AT labri.fr>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] nat_rect?
Date: Thu, 06 Oct 2005 15:28:29 +0900
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: JAIST

Pierre Casteran wrote:

when I check he term you mention on V8.0pl2, I get the message :
The term "P" has type "nat -> Type" while it is expected to have type
"Type"

Yes, the same for 8.0, April 2004. Is it in any way worrying that Coq outputs an untypable term?

Cheers,
/R

[Coq-Club] nat_rect?, Rene Vestergaard
- Re: [Coq-Club] nat_rect?, Pierre Casteran
  - Re: [Coq-Club] nat_rect?, Rene Vestergaard