The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Mike,

On Thu, Nov 05, 2015 at 10:09:59AM -0800, Michael Shulman wrote:
> According to the reference manual,
> 
> https://coq.inria.fr/distrib/current/refman/Reference-Manual021.html#hevea_command308
> 
> "Set Printing Coercion <qualid>." forces coercion denoted by <qualid>
> to be printed.  However, when I use this command (even on 8.5beta2) I
> get "Warning: There is no option Printing Coercion <qualid>."  (where
> of course <qualid> is the name of some coercion already declared).  Am
> I crazy?  Does this command actually exist?

The doc is obsolete. Since 8.2, the new option is

Add Printing Coercion <qualid>.

Sorry,

Hugo