Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Abuse of coercions gives weird results in coqtop.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Abuse of coercions gives weird results in coqtop.


chronological Thread 
  • From: Brandon Moore <brandon_m_moore AT yahoo.com>
  • To: Georgi Guninski <guninski AT guninski.com>
  • Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Abuse of coercions gives weird results in coqtop.
  • Date: Mon, 30 May 2011 11:17:27 -0700 (PDT)
  • Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=Message-ID:X-YMail-OSG:Received:X-Mailer:References:Date:From:Reply-To:Subject:To:Cc:In-Reply-To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=JNughtmeen507uth8EtMEFOC4GuFpZGAFu5LE9QkMxurLzuu6Mj13UUEKrr3/oq8vME4O9TkLDu/Ux8UjViJm+MMH/os+QIKZE7jYRUVljfwCcwS32i5lAjXVJdy1xfD9ksSbNqI01zK4iEdMdgGSYJ/OUXWyA58I/3haDqrvcI=;
> From: Georgi Guninski 
> <guninski AT guninski.com>

> Sent: Monday, May 30, 2011 10:22 AM
>
...
> 
> i asked how to check for cheating proofs.
> 
> Bruno (appears a coq developer) replied:
> https://sympa-roc.inria.fr/wws/arc/coq-club/2011-05/msg00101.html?checked_cas=2
> 
> how a client should check a Coq proof for cheating?
> 
> If I were the client I would disable all customized notations with
> Unset Printing All.  
> ^ Bruno wrote this.
> 
> so i follow his advice:

Oh, he actually had the advice backwards!

It's "Set Printing All" that turns off notations, and starts showing
all coercions, implicit arguments, and other things that may
normally be hidden. ("Unset" goes the other way, and makes things
short but possibly misleading again)

http://coq.inria.fr/refman/Reference-Manual004.html#toc23

You might also set "Set Printing Universes".

Brandon



Archive powered by MhonArc 2.6.16.

Top of Page