The Coq mailing list

[Yann Régis-Gianas <yrg AT pps.univ-paris-diderot.fr>]

This has been implemented in the trunk by Pierre-Marie Pédrot.

➜  coq git:(trunk) ✗ coqtop

Welcome to Coq pangolin:/home/yann/git/research/coq,trunk (851539eca5016da98253308749131abae3ec7b93)

Coq < Parameter t : forall { n : nat }, Type.

t is assumed

Coq < Axiom a : t (n := 0).

a is assumed

Coq < Axiom b : t (n := 1).

b is assumed

Coq < Goal a = b.

Toplevel input, characters 9-10:

> Goal a = b.

>          ^

Error: The term "b" has type "@t 1" while it is expected to have type "@t 0".

Le lun. 29 juin 2015 à 17:05, Pierre Courtieu <pierre.courtieu AT gmail.com> a écrit :

That would be great.

P.

2015-06-29 17:02 GMT+02:00 Jonathan Leivent <jonikelee AT gmail.com>:

On 06/29/2015 10:43 AM, Pierre Courtieu wrote:

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

Is there also a very common corresponding enhancement request: why not have Coq determine whether the two types will be visibly different when printed under the current settings - and if not, temporarily Set Printing All (and say that it is doing so to avoid confusion) in order to display a more meaningful error message - perhaps after first printing the type under current settings so that the user would have an easier time following the correspondence?

-- Jonathan

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.