coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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?
- [Coq-Club] Set Printing Coercion qualid, Michael Shulman, 11/05/2015
- Re: [Coq-Club] Set Printing Coercion qualid, Hugo Herbelin, 11/07/2015
Archive powered by MHonArc 2.6.18.