coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Unset Printing Notations xyz_scope.

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Unset Printing Notations xyz_scope.
Date: Tue, 27 Aug 2019 08:55:37 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f48.google.com
Ironport-phdr: 9a23:njIlORHe4g9b1jVmACx8+Z1GYnF86YWxBRYc798ds5kLTJ7zp8+wAkXT6L1XgUPTWs2DsrQY0rCQ6v2wEjBaqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmssAnctsobjYRtJ6ov1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrx2hqRJxwIDafZ+bO+Zlc6zHYd8XX3BMUtpNWyFDBI63cosBD/AGPeZdt4Twu0ABrRu/BQm3BOPg1DxIjWLq0K08yeshFxzJ1xEnEt0Uq3vUrNT1NLwSUe+rz6nE1y/Mb/VM1jf79YfEaBEhofCQXbJ/asfRxkwvGBnEjlWUs4DqIzSV1uEUvmWd8uFuW+Wvi2s9pAFwpDii3tsjio7ThoIT1F/E8SF5zJwrKtKlVU52Z8OvHphItyyCKYd6XscvT3trtSs60LEKpJ+2cSkQxJkoxBPSbeGMfZKS7RL5TumRJC91hHJ7d7K7gBa/6U2gxff9VsmwyVpKry1FnsTVunAD2BHe6dKLSvR6/kem1jaP0x7c5vtYLkAzkKrXM58hwrgumZoPqUnPADP6lUHsgKKVdkgo4PWk5uXmb7n8qZKRNJd4igTkPaQvnsy/D/44Mg8LX2WD4+uzz73j/UziQLVKkPI2kbPVv4rcJcsBoK62HhVZ0oci6xajADery9sYnXwdI1JEfBKLlZTmO1bLIPzgF/ewn0yskCt3x/DBJrDuHpLNLmHanLj9ebZ99lVTxREozdFf4pJUEqsOLOjyWk/3rtzYDwU2Pxa6w+b9W51B0dYVXnvKCauEOuuGuliRo+krPuOkZYkPuT+7JeJztND0inpssFUdfLKp0JhfQXaxGPgud0yTYXv3gtoCV24MtwwyCu3rlFKqXjtaZnL0VKU5sGJoQLm6BJvOE9j+yIeK2z22S8UPOzJ2T2uUGHKtTL2qHvcBbCXIf51kmz0AELmmEsoviUHouwj9xL5qaOHT/39A7MOx5J1O/+TW0CoK23lxBsWZ3XuKSjgtzGwNTj4ymqt4pB4kkwvR4e1Dm/VdUOdrybZRSA5jbMzTyuV7D5b5XQeTJto=

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