Skip to Content.
Sympa Menu

coq-club - [Coq-Club] skip %Qp, %nat when Printing

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] skip %Qp, %nat when Printing


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] skip %Qp, %nat when Printing
  • Date: Mon, 24 Feb 2025 13:52:17 -0500
  • Authentication-results: mail3-smtp-sop.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-ed1-f45.google.com
  • Ironport-data: A9a23:MDorHay6aVXKeUfS/xp6t+edwirEfRIJ4+MujC+fZmUNrF6WrkUFz GcdWDiBPPvZYWbxKtgjO46x9RkBuMXdz9RrHlY+rVhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefSAOCU5NfsYkhZXRVjRDoqlSVtkus4hp8AqdWiCmthg /uryyHkEAHjgmUc3l48sfrZ9Us15qiq4lv0g3RnDRx1lA+G/5UqJMlHTU2BByOQapVZGOe8W 9HCwNmRlo8O10pF5nuNy94XQ2VSKlLgFVDmZkl+B8BOtiN/Shkaic7XAhazhXB/0F1ll/gpo DlEWAfZpQ0BZsUgk8xFO/VU/r0X0QSrN9YrLFDm2fF/wXEqfFPz/sVJIl42G7QD96VcGmJi8 8wVGSEkO0Xra+KemNpXS8Fpj8UnacTnZcYR5iwmwjbeAvIrB5vERs0m5/cChGZ21p0IR66OI ZZEAdZsREyojxlnM10XCYk+keTuj3/2dTEeqVOJqoI45mHSyEp6172F3N/9I4TbFJ4Lxx/Dz o7A1z/+BDJAZP2x8mKc0H+hiv7K2iPAe51HQdVU8dYx3QTLmT1NYPEMbnOwpuD8gUqjUfpEO kkM82wvq7Iz/QqlVLHAswaQpXeFulsRV4MVHbFnrg6KzaXQ7kCSAW1soiN9hMIOq/IGYhI11 nmwhN6qLidsnLulREOM3+LBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4zQMZZafWlSVnNL yC2kcQou1kEYSc2O0iT+FnGh3ehqsGMQFJooArQWW2h40VyY4vNi22UBbrzvKoowGWxFwbpU J04dy62sr1m4XalynHlfQn1NOv1j8tpyRWF6bKVI7Ev9i6251modp1K7Td1KS9Ba5lYIWa3O hCK41gKufe/2UdGi4cnM+pd7Ox6ncDd+SjNDaC8gidmO8ghK1fYrH0GibC4gTqyzRB0+U3AB XtrWZ3xVC5FWPoPIMueSOAa3rsmjiE4ziW7eHwI50XP7FZqX1bMEe1tGALWMIgRtfrYyC2Lq Yo3H5XRkH13DrauChQ7BKZJcTjm21BhWMiu86S6t4erfmJbJY3WI6WOnOl4Jd01zvs9eyWh1 ijVZ3K0AWHX3RXvQThmoFg6AF82dc8n9i5pDj9mJluyxXkobKCm6apVJdN9fqAq+KYnhbR4R uUMMZfISPleaCX1yxJEZ7nEratmaEuKgyCKNHGbezQRRcNraDHI3d7GRTHR0hcyIBC5juYAh oGx9xj6RMMDTjtyDcyNZ/OIyUiwjEcnm+lzfhXpJ4BTcXrz7LpVEjzVsc5vBfpRLx+Zlz2Q+ DuLME1JucjMvI4H393bjo+Ur4qSMrVfH2gLO0L5/LqJJS3h0W77+rB5UcGMZiL4eFLv3qepd cF57qjbHqUcvVBot4FcLe5a/Zgm7YGym44AnxVWInrbSn+KVJViGyCi9utSvPRvwrR5h1OHa niX8IMHBYTTadLXK39PFg8Lde/Z6Oo1nAPV5vELIEnXwi970b6EcEdKNSm3ly1vA+ppAbwh3 NselpYa2y6nhjouF+S2vCRe2mCPD34HCoEMlJURBq31gQsKlHBGR7HhCRHN3ZLeUOUUb3EWI QKVipHS2JVa5E7JKEQoGVb3gOFyuJUpuTJx9mEkGWinoNT/u6II7EVjyghvFgVx5Tdb4t13I VluZhFUJ73R3jJGh/pjfmGLGiNHDiK34kballkDzjXYa2KKVWX9CnI3FsjQ3UIe8kNaJiN6+ pPBwknbcD/aRuPD9QpsZlxE8tvIUs5U2jDZvvyeD+CpPsUfcCX0pK2Dfk8KoEbXOtwwj0j5u uVaxuZ8RqnlPyo2oadgKY2l+ZkPaRKDNkpQaOpA+f4XIGTiZz2C4ziCBESvcMdrJfaR00uZC dRrF/1fRSaFyyeCgTAKN5Eie4YusqYS2+MDXbf3KUotkbiV9GNpua2N0BnOvjYgRtE2nPstL o/USSm5LVWRonlpgE7IkthPPzupQNsDZTCk5tuPzscyK8shvt1vIGYI6Znlm1WOMQBiwQCYg xObWY/S0N5Z6NpNm6nCL/x9IjuaePLJesaGygSRi+h1TMjuNJ7OvjwFq1O8MAVxO6AQautNl r+MkYDW2U/ZjYkySETcvYeLLIhSxMCIROEMGNnGHHpbuiqjWcHX/BoI/V6jG6FJiN9w4sqGR ROyTcmNKfo5fsh7/2IMTQRzCDMfBLbTQoa6gBiivtKeDhQ5+i7WHuONrHPGQzlSSX4VBsfYF ATxhceL2vlZi4ZpXzovGPBsBs5DEm/JAKcJWYX4imiFMzOOnFiHh7rFkCgg4xHtDl2vMp7zw bDBdyjEWCWCgoP65/AHjNUqpTwSNmh3vscodEFE+9JWtSGzPFRbEcsja6c5GrNmuQ2s8qrnZ QP9TnooUgT8ejVmTS/SwvreWiWnO+hfHeuhexII+RqYZR7jUcnESPFk+zx76nh7Rir7wav1Y ZsC83n3JV6qzosvWe8X4eehjPx6wu/BgEgF4l35j9e4FiN27W/mD5C9NFElue37/8DxeIHjI GE0QSVJTBj+RxKsV8lnfHFRFVcSuzaHI/DEq8uQ6I63hmlZ5LQoJD7D1yXb3bgKbcBML7kLL Z8yb3XY+HiYgxT/poNw0+/EQsZI5TajEc2zLaulTgoX9011BqLLIOta9RcyoAoeFMKz3r8Te vRAI5TzOahdFH1s5Q==
  • Ironport-hdrordr: A9a23:LQx4IKPwOt3/NsBcTuyjsMiBIKoaSvp037BL7TEJdfUxSKalfq +V7ZYmPHPP+VUssRIb+exoWpPwJU80nKQdieIs1NyZLW7bUQWTXedfxLqn7TmlNCH36/JH2b 0ISdkaNPTASXZ/yej1iTPWLz/i+rW6GWKT6Ns2A00CceiiUcBd0zs=
  • Ironport-phdr: A9a23:n0sJkxZNWg3qBz+6qss+A63/LTFW2YqcDmcuAnoPtbtCf+yZ8oj4O wSHvLMx1wWPBd2QtKMZ0KL/iOPJZy8p2dW7jDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgH c5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTezf79+N gm6oRneusQUhYZvKqg8wQbVr3VVfOhb2WxnKVWPkhjm4cu+4IBt+DlKtfI78M5AX6T6f6AmQ rFdET8rLWM76tD1uBfaVQeA6WcSXWsQkhpTHgjK9wr6UYvrsiv7reVyxi+XNtDrQL8uWDSi6 6BrSAL0iCoCKjU0/n3bhtB2galGph+quh5xzJPOYIyNO/Vwfq3Tc9AHS2RfQslcTDZODp+mY oYVE+YNIeRVoo/grFUOtxu+AgysCfvzxzBThn/23LY60+Q/HgHFwQctA9QOv27SrNroKawfV vq6w7LIzTXCdPNW2Sny6IvSfh87p/GDR7RwftfLxUkuFgPFklqQpJfqPzOQzOsNsmyb4/B8W uKojm4qsgd8qSWgyckwkIfGnJ4Vykza+iVjxoY4PcO1Rk5lbNO5H5ZeuDyXO5V4T888QGxlp Cg3xL0YtZO0eCUHyokryhzCZvGHc4aF4BHuWeSNLTtmmn5oe7Gyihi0/EO9xOP8Ucy030xLr ipDitTDqncN1wbV6seZTvt9+l2t1iiS2ADO7OxPPEM6lbLDJpI/3rI9koAfvEfDEyPshkn6k Kybel8r9+Wo7ensf6vrppuBN49vlgHxLL4ulNG+AeU5LAcDR3SX9OKh37P550L5Wq9Fjvgun 6nZrp/aIcMbq7a8AwBP04Yj7w+zACm739gFhHUHIl1IdRKdg4jmPFHOJ//4DfOhjFi2jDhrw PXGMqXgApXLMHfDjK/scahh50NY0gY+ztBS64hKBr0dI///QED8udzAAh88KQO0wuLnCNtn1 oMZXGKCGrWWP7jSsV+J/eIvI/eDZIwPtDnnLfgq/fjugmIjlV8cfKmpwZQXZWu3HvRjOUqZY H7sjs0dHmcNuwoyVOrqh0aaXj5Je3myR7485i08CI++EIvPXpqtj6CZ3CenAp1WYXhLBUyLE XfxbomLR/MMaD+JLcJ6iTwFVb2hS5c72h20tQ/6zaBnLuvO9SECu5Ljzos92+qGnhYrsDdwE s7Vh2qKViR/mn4Cbz4wxqF250JnnASty6991tVSFd1I5/5KGi48PJjQh7hzAdDzQQLMfZGAT l+gTpOnAC0+Zt00yt4KJU16HoPx3Vj4wyO2DupNxPSwD5su//eEt5CQD8N0ynKdkbIkk0FjW cxXc2uvmq948QHXQY/PiUSQ0aiwJuwHxCCY0mCFwCKVuV1AFhZqWPDMV3AefUvbrpLw4ErEQ /mvCKgoGgREwM+GbKBNb46hlk1IEc/qI8+WeGetgyG1DBeMyKmLad/jcWUcxyXQCw4NlQkV8 TCHNBQxLiikqmPaSjdpEAGneFvipM95rn7zVUoo10eKYklmgqKy4QIQjOeARuk727sFvGIsp 2wxEgrgmd3RDNWEqkxqe6A0jcoVxlBB2CqZsgV8OsflNKV+nhsFdBwxuUry1hJxA4EGkM4wr XpswhAgYaSfmEhMcT+Vx/WScvXeN3Xy8RazaqXXxkCW0dCY/b0K4eg5rFOrtR+gF04r+XFqm 9dP1H7U6pLPBQsUGZX/NyR/vxFwp7DBYiQ+oYrS3Htgd6i1rjDq1NcgBe9jwRGlPp9ePK6CC A7uApgCHcH9TY5i01Otbx8CIKVT7PtuZ5LgJ6bAgvb7ero9z1fExSxd7Ytw01yB7X95Q+/Mh NMexu2AmxCAT3H6hUugtcb+ncZFYysTFyyx03uBZsYZa6tscIIMEWrrLdeww4A0jpTtWmVY+ V3lDlUP3sPveBuOYHTy2ARR0QIcpnntyk7ah3Rk1iokqKaSxnmEyu7idQEHN20NTW9ri1uqI ImogPgVWUGpa04ikx7vtiOYj+BL4a94KWfUW0JBeSP7enpjXqWHvb2He8dT6ZksvE27ScyEa EuBAv74qhoeiGb4GndGgSs8b3ess4n4mBpzjCScKmxypTzXY5M4yRDa7d3aDflfu1hODCByi TjMBlW/edCv9NOY0ZbCru+WWGeoV5kVei7uhY+Nryq042R2DAb3xaji3I26V1JigWmnipFjT kCq5F7kb5Pu1rimPO4vZURuCFLmqoJ7Fox4jooslcQV0HkeiI+S+ClPmmPyPNNHnKPmOSBVF HhbnpiPuFijhBAwSxDBj5j0XXic3MZ7MtyzY2dNnzk489gPE6CMqrpNgSpypFO86wPXe/l02 DkHmp5MoDYXhf8EvA01w2CTGLcXSANRNyztjBSF7Ja3qqxRaCCucKS//EV7lNGlSrqFp0sPP RSxModnBiJ24shlZRjF2n3y8YHpe5/Za9sVuluVkgvPp+dQIZM10PENgGA0XAC19W1gwOk9g xt02Ji8t4XSMGRh8pWyBRtAPyH0bcceqXn9yLxTlcGM08WzD41sT38VCYDwQ6viQ1dw/bz3c hyDGzompjKHFKrDSEWBvVx+oSuHEoj3ZSrKYiBIlZM4GEbbfAsF3EgVRGlowMJ/TFvxgpW/K AEhoWlAgzyw4hpUlrA2aV+mCj2Z/EHwLW1sAJmHcEgIsEcYuxaTYZTYtqUpR2lZ5sHz81bLc zDdPlUSSzlOAxzhZRirP6Hyt4actbHCW6zmaaOJOOvGqPQCBa7QldT2jdQgr3DUcZ/Wdnh6U 69ihREFBCElXZyfw3JWFUl132rMd5LJ/k/tvH0q6JnloLKzH1uwrYqXV+kIaIsppkDw2PbZc bbX3XcxKC4EhMlVmzmSk+lZhwRU02Y3JlzPWfwWvCrJBso8g4dxCBgWI2N2PcpMtOcn2xVVf NXckpXz36J5ifg8DxFEU0bgk4enf55CJWb1L17BCEuRUdbObTTW38H6Z7+9QrxMna1VsRO3o zOSD07kOHyKiTDoUxmlNewEgjucOVRSv4S0cxAlDmaGLpquchqgLNp+liE725Uxj3LOcGMQa H1yLx4LobqX4idVxP54Hi0J73ZoK/WFhzfM7+TcLcVz07MjCSB1muRGpXUinuENvWcUGbovw HuU8oM9xjPu2vOCwTdmThdU/zNChYbQ+F5nJb2c7Z5YH3DN4BMK62yUTRUMvdpsTNP16MUyg pDCkrz+LDBa/pfa58wZUoLdIsKGK3osMlzgHjfSAE0ETCKkHW7ajk1Z1vqV8zfGy/py4oipg 5cIRrJBARYtEegGD01+ANEYCJJ+XzdhnLLCycBUuDyxqx7eQMgctZfCHKH3Y72nOHOSir9KY AENyLXzINEIN4H17Edlb0FzgIXAH0e4tT9lrShobwtyq0JIoiEWpowb3kvkbkag7CZWG6Lp2 BExjQR6bKIm8zK+uz/fw3LFoSIxlA86ntC32Vis
  • Ironport-sdr: 67bcc00b_Ehdf/EhttGy5hRxlDQ7rff49fiifejST64/TwUYt9kqtJWC uB07XHcu7Oyi7dHC47L6TpbdsDMZ0C55chC1myg==

Is there a way to ask Coq to skip printing scope keys when printing the goal?
These keys can be helpful to Coq experts doing proofs but can be confusing when explaining the proofs at a high-level to non-Coq-experts.

Regards,


  • [Coq-Club] skip %Qp, %nat when Printing, Abhishek Anand, 02/24/2025

Archive powered by MHonArc 2.6.19+.

Top of Page