The Coq mailing list

[<michael.soegtrop AT intel.com>]

Dear Coq Users,

I don't understand the syntax given in chapter 19.3 of the reference manual:

Instance prod_eqb ‘(EA : EqDec A, EB : EqDec B) : EqDec (A * B)

What is the meaning of the prime here? Is this an abbreviation for this:

Instance prod_eqb {A B : Type} (EA : EqDec A) (EB : EqDec B) : EqDec (A * B)

Also I have problems to make Coq parse the syntax given in the manual with all
3 prime variants on my keyboard (`'´) and the prime used in the manual (‘).
Is there a description for this syntax in the reference manual?

Thanks & Best regards,

Michael