The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

Le 21 nov. 2011 à 04:11, Gyesik Lee 
<gslee AT hknu.ac.kr>
 a écrit :

>> Just removing "in ... return ..." seems to work.
> 
> I am wondering why it doesn't work when "in ... return..." is used.

Adding in ... return deactivates the special treatment of pattern-matching of 
 Program, e.g the implicit threading of equalities in the branches.

>> I was able to fix it by adding "Require Coq.Logic.JMeq" (note just one 
>> .JMeq
>> instead of .JMeq.JMeq) to the top of the file.  Have we just discovered a 
>> minor
>> typo in Coq?
> 
> By "Require Coq.Logic.JMeq" you are importing the JMeq module,
> and that module includes the inductive type JMeq.
> 
> I guess, the JMeq type is implicitly used in dealing with your case.

Indeed, JMeq might be used during the compilation of pattern-matching, that's 
why it is required. I think the anomaly turned into a nicer error message in 
the trunk. Might still be the wrong error message though :)

-- Matthieu