The Coq mailing list

[alexander AT math.ohio-state.edu]

Thanks very much for the quick reply :)

When I tried to remove the "in ... return ..." part, I got this error message:

"Anomaly: Program: cannot find Coq.Logic.JMeq.JMeq. Please report."

(I've uploaded the precise file which produces the error message to
http://www.math.osu.edu/~alexander/variadic/variadic2.txt ;)

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?

Thanks very much, this seems to have done the trick!  Finally my definitions
are squared away, now for the actual proofs to begin...   (crossed fingers!)

-Sam Alexander