The Coq mailing list

[Gyesik Lee <gslee AT hknu.ac.kr>]

> Just removing "in ... return ..." seems to work.

I am wondering why it doesn't work when "in ... return..." is used.

> 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.

Gyesik