The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Michael,

  This prime is a backquote, I think it is described in a section about generalizable variables, or at least the command Generalizable Variables A B which you need here should be in the command index. Didn't you get at least one error saying something close to "unbound and non-generalizable variable A"?

Best,
-- Matthieu

Le mardi 16 décembre 2014, <michael.soegtrop AT intel.com> a écrit :

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

--