coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Unknown type error
- Date: Mon, 29 Jun 2015 16:43:58 +0200
Quick answer (very common question). Try replaying the error after setting this: "Set Printing All."
This will disable the hiding of implicit arguments and notations that make you believe these two types are the same.
Best regards,
Pierre
2015-06-29 16:31 GMT+02:00 Marcus Ramos <marcus.ramos AT univasf.edu.br>:
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, Pierre Courtieu, 06/29/2015
- Re: [Coq-Club] Unknown type error, Jonathan Leivent, 06/29/2015
- Re: [Coq-Club] Unknown type error, Marcus Ramos, 06/29/2015
Archive powered by MHonArc 2.6.18.