The Coq mailing list

[Cyril Cohen <cohen AT crans.org>]

Dear Vladimir, Jason and Ian,

 On 15/02/2014 01:00, Jason Gross wrote:
> So you could do [Notation "'test' x f"
> := (tohfiber f x).], replacing [test] with whatever you want.

Actually putting single quotes around test reserves it as *keyword*, (meaning you 
won't be able to name anything else "test" again, except as a keyword in another 
notation), and I discourage you doing this unless you really meant it to be a new 
keyword of the language.

For now, when you are defining a notation containing no special character I 
advise that you make an abbreviation* instead:
Notation test x f := (tohfiber f x).

Best regards,
--
Cyril Cohen
* http://coq.inria.fr/refman/Reference-Manual014.html#hevea_command268