coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Unknown type error

From: Marcus Ramos <marcus.ramos AT univasf.edu.br>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Unknown type error
Date: Mon, 29 Jun 2015 15:31:10 +0100

Hi,

What should I do when I get the following error message?

"The term "H29" has type "In (inl n) (map inl r')"
 while it is expected to have type "In (inl n) (map inl r')"."

I am using Coq 8.4 pl14 in CoqIDE for Windows 8.

Thanks in advance,
Marcus.

[Coq-Club] Unknown type error, Marcus Ramos, 06/29/2015
- Re: [Coq-Club] Unknown type error, Greg Morrisett, 06/29/2015
- Re: [Coq-Club] Unknown type error, Pierre Courtieu, 06/29/2015
  - Re: [Coq-Club] Unknown type error, Jonathan Leivent, 06/29/2015
    - Re: [Coq-Club] Unknown type error, Pierre Courtieu, 06/29/2015
      - Re: [Coq-Club] Unknown type error, Yann Régis-Gianas, 06/29/2015
- Re: [Coq-Club] Unknown type error, Marcus Ramos, 06/29/2015