Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Unknown type error

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unknown type error


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




Archive powered by MHonArc 2.6.18.

Top of Page