Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Set Printing Coercion qualid

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Set Printing Coercion qualid


Chronological Thread 
  • From: Michael Shulman <shulman AT sandiego.edu>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Set Printing Coercion qualid
  • Date: Thu, 5 Nov 2015 10:09:59 -0800
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=viritrilbia AT gmail.com; spf=Pass smtp.mailfrom=viritrilbia AT gmail.com; spf=None smtp.helo=postmaster AT mail-lb0-f180.google.com
  • Ironport-phdr: 9a23:gN+qqRWZ4/nr1D75hmzpQA6AdyHV8LGtZVwlr6E/grcLSJyIuqrYZhOFt8tkgFKBZ4jH8fUM07OQ6PC9Hzddqsrf+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8CVOFgD2GT1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3SNp41Rr1ADTkgL3t9pIiy7UGCHkOz4S43VXxeuR5VCUCR5xbjG5z1ryHSt+xn2SDcM9egHp4uXjH3yqZgSBbljG88NyM99WjRwphrjL9fpRunjwd2xYLVbY6ScvdyY/WOLpshWWNdU5MJBGR6CYSmYt5KVrJZMA==

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?



Archive powered by MHonArc 2.6.18.

Top of Page