coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unset Printing Notations xyz_scope.

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Unset Printing Notations xyz_scope.
Date: Tue, 27 Aug 2019 18:20:13 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f54.google.com
Ironport-phdr: 9a23:dm59wRbwM72JdOpcOayWqUL/LSx+4OfEezUN459isYplN5qZr8+6bnLW6fgltlLVR4KTs6sC17OM9fm9CSdcvt6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vMhm6txjdu8kVjIdtJas8yAbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDMi7mrZltJ/g75aoBK5phxw3YjUYJ2ONPFjeq/RZM4WSXZdUspUUSFKH4GyYJYVD+cZMulYoYvyqVsAoxW9GAeiGv/gxDBTi3/qxK03yfgtHR3a0AEiGd8FrXTarM/yNKcXSe270qnIyi/Eb/xO2jj96Y3IchU/rvGWWLJ/a8zRyU8yHA7CklWQqZLqPzSP2uUMsmib6u9gVeO0hm4orgF+uDmvxsM2hobVgYIVz0nJ+CNky4g7It24TVR0Yd+iEJZIqy6aMJF2QsU8TGFsvCY20KMJtoOmfCQSx5QnxgLfa/yac4eT+B7sSOGRITJ+iXl4e7y/nw6//Va8xuD4TMW501ZHojBbntXRtH0BzRze58eBR/Bg5EmuwyyP2BrW6uxcIUA7i67bK5k5z741jJUTsEDDEjbomEXtkaOab0sk9+in5uj9bbXmoZicN4Bwig7gKKghhsu/AeEgPggPWWiU5/i82aX98UHlRLhGlP47n6nDvJzEOMgWpLS1Dg9a34o77hawFTam0NAWnXkdK1JFfQqKj5TpO17QJ/D0F/a+g1WpkDduxvDLJbLhApDXIXjClLftZ6py60lZyAYr19BQ+4pUCq0dIPL0QkL+qNvYDgYgPwOox+bnFc5y25gFWWOPB6+ZKLndvUWJ5uIpOemMZZUatCzzK/g/tLbSiioSnkZVVq2019NDY3ehW/9iPk+xYHz2g95HH31c7SQkS+m/tF0DVglhZnO3Urg57zc9QNa6DYrEAJKshbmA9Ci+F5xSIGtBDwbfQj/Ta4yYVqJUO2qpKch7n2lBDOD5Et5z5VSVrAb/joFfAK/R8ywcu4jk0YEsteLWnBA2szdzCpbEijzffyRPhmoNAgQO8uV/rEh6kArR1KF5h7lGDoUW6a4VFAg9MpHYwqpxDNWgAludLOfMc06vR5CdOR90Vsg4moZcbEN0GtHkhRfGjXKn

Hi,

That's currently a feature request
(https://github.com/coq/coq/issues/5591) looking from some volunteer
to address it. Part of the steps are already done.

Théo

Le mar. 27 août 2019 à 17:56, Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
a écrit :
>
> Is there a way to temporarily disable the printing of a group of notations?
> Closing notation scopes only seems to affect parsing, not printing.
>
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/

[Coq-Club] Unset Printing Notations xyz_scope., Abhishek Anand, 08/27/2019
- Re: [Coq-Club] Unset Printing Notations xyz_scope., Théo Zimmermann, 08/27/2019