Skip to Content.
Sympa Menu

coq-club - [Coq-Club] make proof-general/company-coq stop on warnings

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] make proof-general/company-coq stop on warnings


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] make proof-general/company-coq stop on warnings
  • Date: Wed, 5 Jul 2023 14:53:36 -0400
  • 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-lf1-f54.google.com
  • Ironport-data: A9a23:F2MQkaje0GTywfBd6UMOjT/DX161tRQKZh0ujC45NGQN5FlHY01je htvWWCPa/neZmGkLd9yPtznpkkD7ZXdz9QyTFM/+CxgF39jpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqieUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYqdDpNg06/gEk35q+q52tF5gZWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGU2M7bbwq2NtNWGwf8 P4CFT0naBaYmLfjqF67YrEEasULKcDqOMYbtCglw2yFS/khRp/HTuPB4towMDUY3JgfW6aDI ZNHNnwyMHwsYDUXUrsTIJs0nOazhnT8NTReoVSZ46s2/2f7wwl40byrO93QEjCPbZsNwBjI/ z2al4j/KjU3KcCW+CW4yF69uMvDvy3Jfok9DoTto5aGh3XKnjBJYPEMbnOwpuD8gUqjUfpEO kkM82wvq7Iz/QqlVLHAswaQpXeFulsYVYMVHbBmrg6KzaXQ7kCSAW1soiN9hMIO6+07FQ0Y9 GKzxt64AD51jbC/T3SG6eLBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4zQcZZafWlSVnNL yC2QDsW3OpM0JZav0mv1RWW3GL2/8mhohsdv12PBgqYAhVFiJlJjrFEBHDe5PdEaYKXFxyP4 SRClM+Z4+QDS5qKkURhodnh/pn4vZ5p0xWG2jaD+qXNERzzpRZPmqgOvFlDyL9BaJpsRNMQS Ba7VfltzJFSJmC2SqR8fpi8Dc8npYC5S4S1CqGJMoEUO8UoHONiwM2ITR7Bt4wKuBh8+ZzTx b/GGSpRJSxKV/03kGDeqxk1j+F3l0jSOl8/tbiil0j9uVZvTHGSTrgBPTOzghMRvcu5TPHu2 48HbaOikk0BOMWnO3W/2dBJcTgicyNgbbio8Jw/SwJ2ClA5cI3XI6SBn+1Jlk0Mt/g9q9okC VnkChcDkweh2RUq62yiMxheVV8mZr4nxVpTAMDmFQzAN6ELMN33vpQMPYA6Z6cm/+FFxPt5B atNMcaZD/gFDnyN9z0BZNOv5MZvZTa6tzKoZiCFWTkYe4I/Zgrr/tS/QBDj2hNTBQWKtOw/g Yaa6CXlfbQ5ST9PNv3mMMCU8wvpvFw2uv5DYE/TE9wCJGTu6NdLLgLyvN8WIuYNCxPJ+RWC3 S3LAx1C/ejpiK02+envmqqrgdqIEex/P0wCBEjdz++8Ghf791qZ471rcbi3bxGEc0jr6oCOW P5z88jsFNEmwHNbrJtaEZtw6KA1uuvUuL5Ryzp7EEXxb1iEDq1qJl+E15JtspJh66B4uwykf FCm4fhfZKu0Pf36HG4rJAYKavqJ0dcWkGLw6dU3OEDL2z9lzoGYUEl9Pwi+twIFFeFbaLga+ OYGvNIazyediRBwa9aPsX1yxlS2d3cFV/0qi4EeDIrVkTEU81BlY6KNLg/t4ZqKVcdADVlyH B+Qm5j5pup9wmjsTiMNMEbjjMtnuIQ2mRFVzVU9CUyDtfjbi9QWghBA0zQFYT5E7xdA0uhMF HBhHBRuF6ej4wVquZBnWmyyEVtNHy+ip077kQMIsEb7TECYcHPHA0NgGOSK/WEfq3l9eBoC9 p6m6W/VaxTYV+Cv4TkXRmhktO3Fcdx90ibgifKXNZ2JMLdiaAW0n5L0Q3QDriXWJP8YhWrFl LFMx/lxY6iqDhwgifQ3JKfC3ItBVS3eAnJJRMxg26Y7HWv8XjWW8hrWImCTfvJ9HdD7wXWaO edPeP0WDw+f0RyQpA81HaQPer94vMA47eo4J4/EGzQ0jKu9nBFI7rTgrjPzlU06ceVIyMwdE L7cRxiGM26XhEZXpVPzkdl5CjKGRucANSLB37GT0eQWFpg8nvlmXmMs35CV4XiEEgtV0CiFn QHEZp2Mluxr9ptxrtG9DoRCGASGBtfhX8uY8A2IkopvbPGeFezspg8qul3cEAAOBoQoWvNzj qWrjNHs+VHs5ZIabjj8oIaQMIVs/uCwbfpzHuOsC0cChgqEesvnwyVbylCCMZYTze9svJi2d TW3eO6bVIAwSdxC4FZ3diIHMRIWK5qvX5favSnn8si9UEkM4zfmcuGi22TiN1xAVykyPJb7N A/4ltCu6v1cr6VOHBU0PO5nMbApPG7cXbYaSPOpuQm6FmWIhnawionmnzck6hDJDSCKLp+rq 9aNDB3zbw+7t6z03clU+d469AEeCHFmx/I8ZAQB8tpxkCq3F3MCMf9bC5gdF5VIiWbn4fkUv t0WgLcKUk0RnAiocCkQJPzmVwabQ+gAY5L3e2Bv8ESTZCO7QoiHBdONM8umD2heIlPeICOPc LnyOUEc+jC+x5hoQaAY4fnTbSJP2KbB3nxRkaziu5WaPvvdaInmEFRuGQNMUWrMFMSleIAn4 4QqbTgsfXxXgnId3Sqtl7C51f3ZUP7SI+0UUBqy
  • Ironport-hdrordr: A9a23:jjz4DakEeDZ9QS4kqiC6eMiER4bpDfKj3DAbv31ZSRFFG/Fw9/ rEoB3U726MtN9xYgBZpTnuAtjjfZqxz+8X3WBVB9eftWrd1ldATrsSibcKqgeIc0fDH6xmtJ uIGJIOb+EYY2IK6/oSIzPUL/8QhPeC+KCswcHEz3lsSgluL4Vt9R1wBAreMmAefngiOXP0Lv ahDwN8yAaISDAtdN2yAnRAd+Lfp9vN/aiWHSIuNlod8hCHiT7t0KL3DxTd/hp2aUIz/Z4StV PeigT86+GYv+qlxgS07R6p071m3OH5wt9PQPeBkNQRN1zX+3yVWLg=
  • Ironport-phdr: A9a23:cvxASRw7y4/YVOPXCzKvw1BlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z hKZvKom3AaBHd2Cra4e1qyO6+GocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexf7J/I A+roQjTucUbgpZuIbs1xhfVv3dEYetbyX1oKF6Jgxrw+sK894N//ipNvP4s68FPXaLmcqoiU LdWFi4mM2c75M3qsRnMUw6C7WYCX2sVjxRFHRHL4An1UZntvCT6sPF92DSBMs3tUb80QzWi4 Lx1RxLulSwKKiQ28GDTisx3kaJbvBesrAFxzoLIfI2YMud1c6XAdt0YWGVBRN5cWCNBDI2yb IUBEvQPMvpDoobnu1cDtwGzCRWwCO7tzDJDm3/43bc90+QkCQzLwBcvH9IPsHTPrNX6KqQSW v2pwanO1zrDae5Z0ir65YfSaR8hofCMXalwccXPykkjDRnKjlOKpozjIjyZzOUNs2mH7+pvT u+vhGsnpBtwojir3Msjlo7JhocMx13C6C52z5o7K8eiR05nfd6rDoFQtyeCOoZoQs0vXXxlt Sk1xLAbp5K2cjYGxZc7yhPRa/KLbYeF7xbhWeqMIzp1mXJodrK9ihux80Ws1vPwWte33VtJo CdIlMTHuH4K1xzW8MeHS/1981+91jaIzQDT7P9LIUQwlabBNZEu36Mwm5wOukrABi/7gFv6g LOSe0k++eWl6/7rbqjnq5KeLYN5ig7zP6IzkcKlG+s4KBIBX22D9OS8yrLj+Ur5Ta1PjvIsk 6nZtInWJcAVpqKkGgNV3IYu5hmlAzep19QYmnYHLFZbdx6dk4fpPFTOLOj5Dfe5nVusjC9my +7aMrDlGJnALXjOnK38cbt86UNQ0go+wN9H65JREL4BIfbzWkHrtNzfCx80Kxa7zP3nCNV8z YMeWXyAAqyDPKzIt1+H/OQvLPSWaI8UuTb9N/cl6uXhjX88g1AdfK2p0YELZ3C/G/RqO0OZb mH0jdcbDWgKphY+TPDtiFCaTDJff2yyUL4k5jEnFIKmCp/OSZyqgLyYxSu0AplWZn1dBV2XC nfpd4CEW+8WZy6II89hlCYEVbm7RIM72xGurlyy970yJe3NvyYcqJirgNNy/qjYkQw43T1yF cWUlW+XGTJahGQNEhY83KFkoUF+gn6F2K50y6hRH9xS/PNEUUEzM5faw6p7Csz9cg3Ed9aND l2hR4P1UnkKUtstzopWMA5GENK4g0Wbt8LLK7oclrjQQYcx7rqZxH/pYcB013fB0qAlyVggW MpGc2O81eZk7waGIYnPng2CkrqyM7wG1XvE/meC1mqDvwdRVgd2XePEXGwQTkTTpNX9oEjFS uzmEqwpZzNI0tXKMa5WcpvshFRCSu3kPYHXaWKwgGe9BlCBwLqKYMzrenkS9CrYAUkA1QsU+ CXOLhAwUwGmpW+WFzlyDRTvbkfrpPF5s2++R1QowhuiakRg0/+x9EdQi6HADfwU2b0AtWEqr DAc8E+V+dXQBpLAogNgeP4ZetYh+BJc0nqfsQVhP5umJqQkh1gEcg0xsVm8nxNwQp5Nl8Qnt hZIhEJ7NL6Y3VVddjiZwYG4O7vZLXP39QyubKie00/X0dKf8KMCoPoirFCrsAasH0sku3Jpt rsdm3KW5pTRDAcRF5v3W0A7sRl7u77ybSw05oeS3nppcOG1vjLEx9M1Fb490B/zGrUXeKiAF QL0D4gbH530cL1sywXvN0xber0Op8tWd4u8evCL2bCmJrNllTOi1iFc5Zxll1mL72x6Q/LJ2 JAMx7eZ2BGGXnHylgTE0Ii/lIZaaDUVBmf6xzLjAdsbb6dyfJ0LBGToKsu+wNk4hp/xVFZX8 VeiAxUN38rjKn/wJxTtmBZd00gauyntkCG4zid0njJvp6yW2iCIwuX+ezIIP2dKQC9pilKmc u3Wx5gKGUOvaQYujh6s4033krNaqKpIJG7WWU5UfiLyIgmOS4OIv6GZK45K4ZIs6mBMVfikJ EudUvj7qgcb1CXqGy1fwio6fnekoMexkxt/gWObZHF9yRiRMch6xRbE5NHfA/dX1zwKAih5l Tb/CV21Pt3v9tKR35vOqeGxUWu9W4YbK3G6i9Pd8nLluis3XVW2hJXR0pX/HBI/0DPn2tUiT ijOoBvmI8Hq26m8LeN7bxxtDV745dB9H9I2mY8xiZcMnHkC08/NrDxXzCGqb4odhP6tCRhFD SQGyNPU/gX/jUhqL3bSgpn8Sm3Y2cx5Id+zfmIR3Cs5qcFMEqadqrJezk4X6hK1qxzcZf9lk 3IT0/wrvTQTieEIowogzWOUBLkUEQ9ZPDDjvxuN5tG66q5QYSz8FNr4nFo7ht2nALyY90tVU nb4YZcvHml56Mx5PBTN0WH8wo7hcdjUK9kUs1fH9nWIx/gQI5U3mP0QgCNhMm+opnwpxdkwi hl21I27toyKeC19ubi0CRlCOnjpdtser3vz2L1GkJ/cjOXNVt1xXy8GV5zyQbe0HSIO4L75Y h2WHmR0q2/HS+GCW1bOsAE88y2JS9fxazmWPCVLk4kkHkLGYhUB2EZMG2xr+/xxXgGymJ6/L gEgvmpXvhig7UEUguNwa0uhDCGF+FbuOm9yEN/FdFJX9l0QuB2TaJDYt7MpWXkfp83EzkTFK 3THNVsUSzhTBwrcQQikZ+fm5MGcobHAVqzncKSIMfPW7rYHH/aQmcD2jdAgpmfQcJ3JZj47U ZhZkgJCRSwrQZyI3WVSDXVNx2SVKJfE7Bakpn8t9575raStAVO1o9PIUuoaMM0zqUrv3+HZb L/W33w/cXEBh/ZujTfewbwbljb+kglIcD+gWfQFvC/JF+fLn7NPSgUcc2V1PddJ6KQ12k9MP 9Tag5X7zOwwiPl9EFpDWVH7/6PhLcUXP2GwMk/GD0eXJfyHIzPM2cT+faK7T/VZkuxVsxS6v TvTHVXkO3yPkDzgVhbnNu8p7mnTJBtFpIS0aQpgE0DmRdPiLxm1aZp50GFwzroziXfHc2UbN Hk0ck9AqKGR8TINgvh7HD8kjDItJu2FliCFqujAf8xO4L07X2Ityb0cvShprtkdpDtJT/F0h ibI+9tnolX91/KK1iIiSx1W7DBCmIOMu0xmf6Tf7JhJH3jer3dvpS2dDQoHo9x9B5jhoadVn 5LGnqLyMzdP8JTd+8IaC47VKd6IGHUkOBvtXjXTCUFWKFzjfXGanEFbnPyIozeNqYMmr5H3h JcUYrpSVVhwEv1DT0o4QJoNJ5B4Wj5imrmexp1thzL2vFzaQ8NUuYrCX/SZDKD0KTqXurJDY gMB3bLyKYl73mzT3kVjbhx+kt2PFReMG99KpSJlY0k/p0AfqBCWoUU83kvkbkWm53pBTJZce zY5jwJ/ZaIm8zK+uz8K
  • Ironport-sdr: 64a5bc56_4mke4nbAZNp1wTrd/An2tUn4k/jWbviotOzi5v0ZQ2cGTYx fB2N2WbO9zshcOiEhWR4quUcr5OudpBXKgrSUvw==

Is there a way I can get proof-process-buffer or proof-goto-point to stop at warnings, similar to how they stop at errors? 
Unlike errors, maybe PG can then let the user single step warnings.





Archive powered by MHonArc 2.6.19+.

Top of Page